Logiweb dictionary of equivalence-relations

Up Help

0	0	equivalence-relations
1	0	cdots
2	0	object-var
3	0	ex-var
4	0	ph-var
5	0	vaerdi
6	0	variabel
7	1	op {MissingArg} end op
8	2	op2 {MissingArg} comma {MissingArg} end op2
9	2	define-equal {MissingArg} comma {MissingArg} end equal
10	1	contains-empty {MissingArg} end empty
11	2	1deduction {MissingArg} conclude {MissingArg} end 1deduction
12	2	1deduction zero {MissingArg} conclude {MissingArg} end 1deduction
13	3	1deduction side {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
14	3	1deduction one {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
15	3	1deduction two {MissingArg} conclude {MissingArg} condition {MissingArg} end 1deduction
16	4	1deduction three {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
17	4	1deduction four {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
18	4	1deduction four star {MissingArg} conclude {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
19	3	1deduction five {MissingArg} condition {MissingArg} bound {MissingArg} end 1deduction
20	4	1deduction six {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
21	4	1deduction six star {MissingArg} conclude {MissingArg} exception {MissingArg} bound {MissingArg} end 1deduction
22	1	1deduction seven {MissingArg} end 1deduction
23	2	1deduction eight {MissingArg} bound {MissingArg} end 1deduction
24	2	1deduction eight star {MissingArg} bound {MissingArg} end 1deduction
25	0	ex1
26	0	ex2
27	0	ex10
28	0	ex20
29	1	existential var {MissingArg} end var
30	1	{MissingArg} is existential var
31	4	exist-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
32	4	exist-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
33	4	exist-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
34	4	exist-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
35	0	placeholder-var1
36	0	placeholder-var2
37	0	placeholder-var3
38	1	placeholder-var {MissingArg} end var
39	1	{MissingArg} is placeholder-var
40	4	ph-sub {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
41	4	ph-sub0 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
42	4	ph-sub1 {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
43	4	ph-sub* {MissingArg} is {MissingArg} where {MissingArg} is {MissingArg} end sub
44	0	var big set
45	0	object big set
46	0	meta big set
47	0	zermelo empty set
48	0	system zf
49	0	1rule mp
50	0	1rule gen
51	0	1rule repetition
52	0	1rule ad absurdum
53	0	1rule deduction
54	0	1rule exist intro
55	0	axiom extensionality
56	0	axiom empty set
57	0	axiom pair definition
58	0	axiom union definition
59	0	axiom power definition
60	0	axiom separation definition
61	0	cheating axiom all disjoint
62	0	prop lemma add double neg
63	0	prop lemma remove double neg
64	0	prop lemma and commutativity
65	0	prop lemma auto imply
66	0	prop lemma contrapositive
67	0	prop lemma first conjunct
68	0	prop lemma second conjunct
69	0	prop lemma from contradiction
70	0	prop lemma from disjuncts
71	0	prop lemma iff commutativity
72	0	prop lemma iff first
73	0	prop lemma iff second
74	0	prop lemma imply transitivity
75	0	prop lemma join conjuncts
76	0	prop lemma mp2
77	0	prop lemma mp3
78	0	prop lemma mp4
79	0	prop lemma mp5
80	0	prop lemma mt
81	0	prop lemma negative mt
82	0	prop lemma technicality
83	0	prop lemma weakening
84	0	prop lemma weaken or first
85	0	prop lemma weaken or second
86	0	lemma formula2pair
87	0	lemma pair2formula
88	0	lemma formula2union
89	0	lemma union2formula
90	0	lemma formula2separation
91	0	lemma separation2formula
92	0	lemma subset in power set
93	0	lemma power set is subset0
94	0	lemma power set is subset
95	0	lemma power set is subset0-switch
96	0	lemma power set is subset-switch
97	0	lemma set equality suff condition
98	0	lemma set equality suff condition(t)0
99	0	lemma set equality suff condition(t)
100	0	lemma set equality skip quantifier
101	0	lemma set equality nec condition
102	0	lemma reflexivity0
103	0	lemma reflexivity
104	0	lemma symmetry0
105	0	lemma symmetry
106	0	lemma transitivity0
107	0	lemma transitivity
108	0	lemma er is reflexive
109	0	lemma er is symmetric
110	0	lemma er is transitive
111	0	lemma empty set is subset
112	0	lemma member not empty0
113	0	lemma member not empty
114	0	lemma unique empty set0
115	0	lemma unique empty set
116	0	lemma =reflexivity
117	0	lemma =symmetry
118	0	lemma =transitivity0
119	0	lemma =transitivity
120	0	lemma transfer ~is0
121	0	lemma transfer ~is
122	0	lemma pair subset0
123	0	lemma pair subset1
124	0	lemma pair subset
125	0	lemma same pair
126	0	lemma same singleton
127	0	lemma union subset
128	0	lemma same union
129	0	lemma separation subset
130	0	lemma same separation
131	0	lemma same binary union
132	0	lemma intersection subset
133	0	lemma same intersection
134	0	lemma auto member
135	0	lemma eq-system not empty0
136	0	lemma eq-system not empty
137	0	lemma eq subset0
138	0	lemma eq subset
139	0	lemma equivalence nec condition0
140	0	lemma equivalence nec condition
141	0	lemma none-equivalence nec condition0
142	0	lemma none-equivalence nec condition1
143	0	lemma none-equivalence nec condition
144	0	lemma equivalence class is subset
145	0	lemma equivalence classes are disjoint
146	0	lemma all disjoint
147	0	lemma all disjoint-imply
148	0	lemma bs subset union(bs/r)
149	0	lemma union(bs/r) subset bs
150	0	lemma union(bs/r) is bs
151	0	theorem eq-system is partition
152	2	eq-system of {MissingArg} modulo {MissingArg}
153	2	intersection {MissingArg} comma {MissingArg} end intersection
154	1	union {MissingArg} end union
155	2	binary-union {MissingArg} comma {MissingArg} end union
156	1	power {MissingArg} end power
157	1	zermelo singleton {MissingArg} end singleton
158	2	zermelo pair {MissingArg} comma {MissingArg} end pair
159	2	zermelo ordered pair {MissingArg} comma {MissingArg} end pair
160	2	{MissingArg} zermelo in {MissingArg}
161	3	{MissingArg} is related to {MissingArg} under {MissingArg}
162	2	{MissingArg} is reflexive relation in {MissingArg}
163	2	{MissingArg} is symmetric relation in {MissingArg}
164	2	{MissingArg} is transitive relation in {MissingArg}
165	2	{MissingArg} is equivalence relation in {MissingArg}
166	3	equivalence class of {MissingArg} in {MissingArg} modulo {MissingArg}
167	2	{MissingArg} is partition of {MissingArg}
168	2	{MissingArg} zermelo is {MissingArg}
169	2	{MissingArg} is subset of {MissingArg}
170	1	not0 {MissingArg}
171	2	{MissingArg} zermelo ~in {MissingArg}
172	2	{MissingArg} zermelo ~is {MissingArg}
173	2	{MissingArg} and0 {MissingArg}
174	2	{MissingArg} or0 {MissingArg}
175	2	{MissingArg} iff {MissingArg}
176	2	the set of ph in {MissingArg} such that {MissingArg} end set