Metamath Proof Explorer

Table of Contents - 2.1. ZF Set Theory - start with the Axiom of Extensionality

Introduce the Axiom of Extensionality
1. ax-ext
2. axexte
3. axextg
4. axextb
5. axextmo
6. nulmo
Classes
1. Class abstractions
2. Class equality
3. Class membership
4. Elementary properties of class abstractions
Class form not-free predicate
1. wnfc
2. nfcjust
3. df-nfc
4. nfci
5. nfcii
6. nfcr
7. nfcrALT
8. nfcri
9. nfcd
10. nfcrd
11. nfcriOLD
12. nfcriOLDOLD
13. nfcrii
14. nfcriiOLD
15. nfcriOLDOLDOLD
16. nfceqdf
17. nfceqdfOLD
18. nfceqi
19. nfcxfr
20. nfcxfrd
21. nfcv
22. nfcvd
23. nfab1
24. nfnfc1
25. clelsb3fw
26. clelsb3f
27. nfab
28. nfabg
29. nfaba1
30. nfaba1g
31. nfeqd
32. nfeld
33. nfnfc
34. nfeq
35. nfel
36. nfeq1
37. nfel1
38. nfeq2
39. nfel2
40. drnfc1
41. drnfc1OLD
42. drnfc2
43. drnfc2OLD
44. nfabdw
45. nfabdwOLD
46. nfabd
47. nfabd2
48. dvelimdc
49. dvelimc
50. nfcvf
51. nfcvf2
52. cleqf
53. abid2f
54. abeq2f
55. sbabel
Negated equality and membership
1. Negated equality
2. Negated membership
Restricted quantification
1. wral
2. wrex
3. wreu
4. wrmo
5. crab
6. df-ral
7. df-rex
8. df-reu
9. df-rmo
10. df-rab
11. rgen
12. ralel
13. rgenw
14. rgen2w
15. mprg
16. mprgbir
17. alral
18. raln
19. ral2imi
20. ralimi2
21. ralimia
22. ralimiaa
23. ralimi
24. 2ralimi
25. ralim
26. ralbii2
27. ralbiia
28. ralbii
29. 2ralbii
30. ralbi
31. ralanid
32. r19.26
33. r19.26-2
34. r19.26-3
35. r19.26m
36. ralbiim
37. r19.21v
38. ralimdv2
39. ralimdva
40. ralimdv
41. ralimdvva
42. hbralrimi
43. ralrimiv
44. ralrimiva
45. ralrimivw
46. r19.27v
47. r19.28v
48. ralrimdv
49. ralrimdva
50. ralrimivv
51. ralrimivva
52. ralrimivvva
53. ralrimdvv
54. ralrimdvva
55. ralbidv2
56. ralbidva
57. ralbidv
58. 2ralbidva
59. 2ralbidv
60. r2allem
61. r2al
62. r3al
63. rgen2
64. rgen3
65. rsp
66. rspa
67. rspec
68. r19.21bi
69. r19.21be
70. rspec2
71. rspec3
72. rsp2
73. r19.21t
74. r19.21
75. ralrimi
76. ralimdaa
77. ralrimd
78. nfra1
79. hbra1
80. hbral
81. r2alf
82. nfraldw
83. nfraldwOLD
84. nfrald
85. nfralw
86. nfral
87. nfra2w
88. nfra2wOLD
89. nfra2
90. rgen2a
91. ralbida
92. ralbid
93. 2ralbida
94. raleqbii
95. ralcom4
96. ralnex
97. dfral2
98. rexnal
99. dfrex2
100. rexex
101. rexim
102. rexbi
103. reximia
104. reximi
105. reximi2
106. rexbii2
107. rexbiia
108. rexbii
109. 2rexbii
110. rexcom4
111. 2ex2rexrot
112. rexcom4a
113. rexanid
114. r19.29
115. r19.29r
116. r19.29imd
117. rexnal2
118. rexnal3
119. ralnex2
120. ralnex3
121. ralinexa
122. rexanali
123. nrexralim
124. risset
125. nelb
126. nrex
127. nrexdv
128. reximdv2
129. reximdvai
130. reximdv
131. reximdva
132. reximddv
133. reximssdv
134. reximdvva
135. reximddv2
136. r19.23v
137. rexlimiv
138. rexlimiva
139. rexlimivw
140. rexlimdv
141. rexlimdva
142. rexlimdvaa
143. rexlimdv3a
144. rexlimdva2
145. r19.29an
146. r19.29a
147. rexlimdvw
148. rexlimddv
149. rexlimivv
150. rexlimdvv
151. rexlimdvva
152. rexbidv2
153. rexbidva
154. rexbidv
155. 2rexbiia
156. 2rexbidva
157. 2rexbidv
158. rexralbidv
159. r2exlem
160. r2ex
161. rspe
162. rsp2e
163. nfre1
164. nfrexd
165. nfrexdg
166. nfrex
167. nfrexg
168. reximdai
169. reximd2a
170. r19.23t
171. r19.23
172. rexlimi
173. rexlimd2
174. rexlimd
175. rexbida
176. rexbidvaALT
177. rexbid
178. rexbidvALT
179. ralrexbid
180. ralrexbidOLD
181. r19.12
182. r2exf
183. rexeqbii
184. reuanid
185. rmoanid
186. r19.29af2
187. r19.29af
188. 2r19.29
189. r19.29d2r
190. r19.29vva
191. r19.30
192. r19.32v
193. r19.35
194. r19.36v
195. r19.37
196. r19.37v
197. r19.40
198. r19.41v
199. r19.41
200. r19.41vv
201. r19.42v
202. r19.43
203. r19.44v
204. r19.45v
205. ralcom
206. rexcom
207. ralcomf
208. rexcomf
209. ralcom13
210. rexcom13
211. ralrot3
212. rexrot4
213. ralcom2
214. ralcom3
215. reeanlem
216. reean
217. reeanv
218. 3reeanv
219. 2ralor
220. nfreu1
221. nfrmo1
222. nfreud
223. nfrmod
224. nfreuw
225. nfrmow
226. nfreu
227. nfrmo
228. rabid
229. rabrab
230. rabidim1
231. rabid2
232. rabid2f
233. rabbi
234. nfrab1
235. nfrabw
236. nfrab
237. reubida
238. reubidva
239. reubidv
240. reubiia
241. reubii
242. rmobida
243. rmobidva
244. rmobidv
245. rmobiia
246. rmobii
247. raleqf
248. rexeqf
249. reueq1f
250. rmoeq1f
251. raleqbidv
252. rexeqbidv
253. raleqbidvv
254. rexeqbidvv
255. raleqbi1dv
256. rexeqbi1dv
257. raleq
258. rexeq
259. reueq1
260. rmoeq1
261. raleqi
262. rexeqi
263. raleqdv
264. rexeqdv
265. reueqd
266. rmoeqd
267. raleqbid
268. rexeqbid
269. raleqbidva
270. rexeqbidva
271. raleleq
272. raleleqALT
273. moel
274. mormo
275. reu5
276. reurex
277. 2reu2rex
278. reurmo
279. rmo5
280. nrexrmo
281. reueubd
282. cbvralfw
283. cbvralfwOLD
284. cbvrexfw
285. cbvralf
286. cbvrexf
287. cbvralw
288. cbvrexw
289. cbvreuw
290. cbvrmow
291. cbvrmowOLD
292. cbvral
293. cbvrex
294. cbvreu
295. cbvrmo
296. cbvralvw
297. cbvrexvw
298. cbvrmovw
299. cbvreuvw
300. cbvreuvwOLD
301. cbvralv
302. cbvrexv
303. cbvreuv
304. cbvrmov
305. cbvraldva2
306. cbvrexdva2
307. cbvraldva
308. cbvrexdva
309. cbvral2vw
310. cbvrex2vw
311. cbvral3vw
312. cbvral2v
313. cbvrex2v
314. cbvral3v
315. cbvralsvw
316. cbvrexsvw
317. cbvralsv
318. cbvrexsv
319. sbralie
320. rabbiia
321. rabbii
322. rabbida
323. rabbid
324. rabbidva2
325. rabbia2
326. rabbidva
327. rabbidvaOLD
328. rabbidv
329. rabeqf
330. rabeqi
331. rabeqiOLD
332. rabeq
333. rabeqdv
334. rabeqbidv
335. rabeqbidva
336. rabeq2i
337. rabswap
338. cbvrabw
339. cbvrab
340. cbvrabv
341. rabrabi
342. rabeqcda
343. ralrimia
344. ralimda
The universal class
1. cvv
2. vjust
3. df-v
4. dfv2
5. vex
6. vexOLD
7. elv
8. elvd
9. el2v
10. eqv
11. eqvf
12. abv
13. abvALT
14. isset
15. issetf
16. isseti
17. issetri
18. eqvisset
19. elex
20. elexi
21. elexd
22. elex2
23. elex22
24. prcnel
25. ralv
26. rexv
27. reuv
28. rmov
29. rabab
30. rexcom4b
31. ceqsalt
32. ceqsralt
33. ceqsalg
34. ceqsalgALT
35. ceqsal
36. ceqsalv
37. ceqsalvOLD
38. ceqsralv
39. ceqsralvOLD
40. gencl
41. 2gencl
42. 3gencl
43. cgsexg
44. cgsex2g
45. cgsex4g
46. cgsex4gOLD
47. ceqsex
48. ceqsexv
49. ceqsexv2d
50. ceqsex2
51. ceqsex2v
52. ceqsex3v
53. ceqsex4v
54. ceqsex6v
55. ceqsex8v
56. gencbvex
57. gencbvex2
58. gencbval
59. sbhypf
60. vtoclgft
61. vtoclgftOLD
62. vtocldf
63. vtocld
64. vtocldOLD
65. vtocl2d
66. vtoclf
67. vtocl
68. vtoclALT
69. vtocl2
70. vtocl3
71. vtoclb
72. vtoclgf
73. vtoclg1f
74. vtoclg
75. vtoclgOLD
76. vtoclbg
77. vtocl2gf
78. vtocl3gf
79. vtocl2g
80. vtoclgaf
81. vtoclga
82. vtocl2ga
83. vtocl2gaf
84. vtocl3gaf
85. vtocl3ga
86. vtocl4g
87. vtocl4ga
88. vtocleg
89. vtoclegft
90. vtoclef
91. vtocle
92. vtoclri
93. spcimgft
94. spcgft
95. spcimgf
96. spcimegf
97. spcgf
98. spcegf
99. spcimdv
100. spcdv
101. spcimedv
102. spcgv
103. spcegv
104. spcedv
105. spc2egv
106. spc2gv
107. spc2ed
108. spc2d
109. spc3egv
110. spc3gv
111. spcv
112. spcev
113. spc2ev
114. rspct
115. rspcdf
116. rspc
117. rspce
118. rspcimdv
119. rspcimedv
120. rspcdv
121. rspcedv
122. rspcebdv
123. rspcv
124. rspcvOLD
125. rspccv
126. rspcva
127. rspccva
128. rspcev
129. rspcevOLD
130. rspcdva
131. rspcedvd
132. rspcime
133. rspceaimv
134. rspcedeq1vd
135. rspcedeq2vd
136. rspc2
137. rspc2gv
138. rspc2v
139. rspc2va
140. rspc2ev
141. rspc3v
142. rspc3ev
143. rspceeqv
144. ralxpxfr2d
145. rexraleqim
146. eqvincg
147. eqvinc
148. eqvincf
149. alexeqg
150. ceqex
151. ceqsexg
152. ceqsexgv
153. ceqsexgvOLD
154. ceqsrexv
155. ceqsrexbv
156. ceqsrex2v
157. clel2g
158. clel2gOLD
159. clel2
160. clel3g
161. clel3
162. clel4g
163. clel4
164. clel4OLD
165. clel5
166. pm13.183
167. rr19.3v
168. rr19.28v
169. elabgt
170. elabgf
171. elabf
172. elabgw
173. elab2gw
174. elabg
175. elab
176. elab2g
177. elabd
178. elab2
179. elab4g
180. elab3gf
181. elab3g
182. elab3
183. elrabi
184. elrabiOLD
185. elrabf
186. rabtru
187. rabeqc
188. elrab3t
189. elrab
190. elrab3
191. elrabd
192. elrab2
193. elrab2w
194. ralab
195. ralrab
196. rexab
197. rexrab
198. ralab2
199. ralab2OLD
200. ralrab2
201. rexab2
202. rexab2OLD
203. rexrab2
204. abidnf
205. dedhb
206. nelrdva
207. eqeu
208. moeq
209. eueq
210. eueqi
211. eueq2
212. eueq3
213. moeq3
214. mosub
215. mo2icl
216. mob2
217. moi2
218. mob
219. moi
220. morex
221. euxfr2w
222. euxfrw
223. euxfr2
224. euxfr
225. euind
226. reu2
227. reu6
228. reu3
229. reu6i
230. eqreu
231. rmo4
232. reu4
233. reu7
234. reu8
235. rmo3f
236. rmo4f
237. reu2eqd
238. reueq
239. rmoeq
240. rmoan
241. rmoim
242. rmoimia
243. rmoimi
244. rmoimi2
245. 2reu5a
246. reuimrmo
247. 2reuswap
248. 2reuswap2
249. reuxfrd
250. reuxfr
251. reuxfr1d
252. reuxfr1ds
253. reuxfr1
254. reuind
255. 2rmorex
256. 2reu5lem1
257. 2reu5lem2
258. 2reu5lem3
259. 2reu5
260. 2reurex
261. 2reurmo
262. 2rmoswap
263. 2rexreu
Conditional equality (experimental)
1. wcdeq
2. df-cdeq
3. cdeqi
4. cdeqri
5. cdeqth
6. cdeqnot
7. cdeqal
8. cdeqab
9. cdeqal1
10. cdeqab1
11. cdeqim
12. cdeqcv
13. cdeqeq
14. cdeqel
15. nfcdeq
16. nfccdeq
Russell's Paradox
1. rru
2. rruOLD
3. ru
Proper substitution of classes for sets
1. wsbc
2. df-sbc
3. dfsbcq
4. dfsbcq2
5. sbsbc
6. sbceq1d
7. sbceq1dd
8. sbceqbid
9. sbc8g
10. sbc2or
11. sbcex
12. sbceq1a
13. sbceq2a
14. spsbc
15. spsbcd
16. sbcth
17. sbcthdv
18. sbcid
19. nfsbc1d
20. nfsbc1
21. nfsbc1v
22. nfsbcdw
23. nfsbcw
24. sbccow
25. nfsbcd
26. nfsbc
27. sbcco
28. sbcco2
29. sbc5
30. sbc5ALT
31. sbc6g
32. sbc6
33. sbc7
34. cbvsbcw
35. cbvsbcvw
36. cbvsbc
37. cbvsbcv
38. sbciegft
39. sbciegf
40. sbcieg
41. sbcie2g
42. sbcie
43. sbciedf
44. sbcied
45. sbcied2
46. elrabsf
47. eqsbc3
48. sbcng
49. sbcimg
50. sbcan
51. sbcor
52. sbcbig
53. sbcn1
54. sbcim1
55. sbcbid
56. sbcbidv
57. sbcbidvOLD
58. sbcbii
59. sbcbi1
60. sbcbi2
61. sbcbi2OLD
62. sbcal
63. sbcex2
64. sbceqal
65. sbeqalb
66. eqsbc3r
67. sbc3an
68. sbcel1v
69. sbcel2gv
70. sbcel21v
71. sbcimdv
72. sbctt
73. sbcgf
74. sbc19.21g
75. sbcg
76. sbcgfi
77. sbc2iegf
78. sbc2ie
79. sbc2iedv
80. sbc3ie
81. sbccomlem
82. sbccom
83. sbcralt
84. sbcrext
85. sbcralg
86. sbcrex
87. sbcreu
88. reu8nf
89. sbcabel
90. rspsbc
91. rspsbca
92. rspesbca
93. spesbc
94. spesbcd
95. sbcth2
96. ra4v
97. ra4
98. rmo2
99. rmo2i
100. rmo3
101. rmob
102. rmoi
103. rmob2
104. rmoi2
105. rmoanim
106. rmoanimALT
107. reuan
108. 2reu1
109. 2reu2
Proper substitution of classes for sets into classes
1. csb
2. df-csb
3. csb2
4. csbeq1
5. csbeq1d
6. csbeq2
7. csbeq2d
8. csbeq2dv
9. csbeq2i
10. csbeq12dv
11. cbvcsbw
12. cbvcsb
13. cbvcsbv
14. csbid
15. csbeq1a
16. csbcow
17. csbco
18. csbtt
19. csbconstgf
20. csbconstg
21. csbgfi
22. csbconstgi
23. nfcsb1d
24. nfcsb1
25. nfcsb1v
26. nfcsbd
27. nfcsbw
28. nfcsb
29. csbhypf
30. csbiebt
31. csbiedf
32. csbieb
33. csbiebg
34. csbiegf
35. csbief
36. csbie
37. csbied
38. csbied2
39. csbie2t
40. csbie2
41. csbie2g
42. cbvrabcsfw
43. cbvralcsf
44. cbvrexcsf
45. cbvreucsf
46. cbvrabcsf
47. cbvralv2
48. cbvrexv2
49. vtocl2dOLD
50. rspc2vd
Define basic set operations and relations
1. cdif
2. cun
3. cin
4. wss
5. wpss
6. difjust
7. df-dif
8. unjust
9. df-un
10. injust
11. df-in
12. dfin5
13. dfdif2
14. eldif
15. eldifd
16. eldifad
17. eldifbd
18. elneeldif
19. velcomp
20. elin
Subclasses and subsets
1. df-ss
2. dfss
3. df-pss
4. dfss2
5. dfss2OLD
6. dfss3
7. dfss6
8. dfss2f
9. dfss3f
10. nfss
11. ssel
12. sselOLD
13. ssel2
14. sseli
15. sselii
16. sseldi
17. sseld
18. sselda
19. sseldd
20. ssneld
21. ssneldd
22. ssriv
23. ssrd
24. ssrdv
25. sstr2
26. sstr
27. sstri
28. sstrd
29. sstrid
30. sstrdi
31. sylan9ss
32. sylan9ssr
33. eqss
34. eqssi
35. eqssd
36. sssseq
37. eqrd
38. eqri
39. eqelssd
40. ssid
41. ssidd
42. ssv
43. sseq1
44. sseq2
45. sseq12
46. sseq1i
47. sseq2i
48. sseq12i
49. sseq1d
50. sseq2d
51. sseq12d
52. eqsstri
53. eqsstrri
54. sseqtri
55. sseqtrri
56. eqsstrd
57. eqsstrrd
58. sseqtrd
59. sseqtrrd
60. 3sstr3i
61. 3sstr4i
62. 3sstr3g
63. 3sstr4g
64. 3sstr3d
65. 3sstr4d
66. eqsstrid
67. eqsstrrid
68. sseqtrdi
69. sseqtrrdi
70. sseqtrid
71. sseqtrrid
72. eqsstrdi
73. eqsstrrdi
74. eqimss
75. eqimss2
76. eqimssi
77. eqimss2i
78. nssne1
79. nssne2
80. nss
81. nelss
82. ssrexf
83. ssrmof
84. ssralv
85. ssrexv
86. ss2ralv
87. ss2rexv
88. ralss
89. rexss
90. ss2ab
91. abss
92. ssab
93. ssabral
94. ss2abdv
95. ss2abdvALT
96. ss2abdvOLD
97. ss2abi
98. ss2abiOLD
99. abssdv
100. abssi
101. ss2rab
102. rabss
103. ssrab
104. ssrabdv
105. rabssdv
106. ss2rabdv
107. ss2rabi
108. rabss2
109. ssab2
110. ssrab2
111. ssrab2OLD
112. ssrab3
113. rabssrabd
114. ssrabeq
115. rabssab
116. uniiunlem
117. dfpss2
118. dfpss3
119. psseq1
120. psseq2
121. psseq1i
122. psseq2i
123. psseq12i
124. psseq1d
125. psseq2d
126. psseq12d
127. pssss
128. pssne
129. pssssd
130. pssned
131. sspss
132. pssirr
133. pssn2lp
134. sspsstri
135. ssnpss
136. psstr
137. sspsstr
138. psssstr
139. psstrd
140. sspsstrd
141. psssstrd
142. npss
143. ssnelpss
144. ssnelpssd
145. ssexnelpss
The difference, union, and intersection of two classes
1. The difference of two classes
2. The union of two classes
3. The intersection of two classes
4. The symmetric difference of two classes
5. Combinations of difference, union, and intersection of two classes
6. Class abstractions with difference, union, and intersection of two classes
7. Restricted uniqueness with difference, union, and intersection
The empty set
1. c0
2. df-nul
3. dfnul4
4. dfnul2
5. dfnul3
6. dfnul2OLD
7. dfnul3OLD
8. dfnul4OLD
9. noel
10. noelOLD
11. nel02
12. n0i
13. ne0i
14. ne0d
15. n0ii
16. ne0ii
17. vn0
18. vn0ALT
19. eq0f
20. neq0f
21. n0f
22. eq0
23. eq0ALT
24. neq0
25. n0
26. eq0OLDOLD
27. neq0OLD
28. n0OLD
29. nel0
30. reximdva0
31. rspn0
32. rspn0OLD
33. n0rex
34. ssn0rex
35. n0moeu
36. rex0
37. reu0
38. rmo0
39. 0el
40. n0el
41. eqeuel
42. ssdif0
43. difn0
44. pssdifn0
45. pssdif
46. ndisj
47. difin0ss
48. inssdif0
49. difid
50. difidALT
51. dif0
52. ab0
53. ab0OLD
54. ab0ALT
55. dfnf5
56. ab0orv
57. ab0orvALT
58. abn0
59. abn0OLD
60. rab0
61. rabeq0w
62. rabeq0
63. rabn0
64. rabxm
65. rabnc
66. elneldisj
67. elnelun
68. un0
69. in0
70. 0un
71. 0in
72. inv1
73. unv
74. 0ss
75. ss0b
76. ss0
77. sseq0
78. ssn0
79. 0dif
80. abf
81. abfOLD
82. eq0rdv
83. eq0rdvALT
84. csbprc
85. csb0
86. csb0OLD
87. sbcel12
88. sbceqg
89. sbceqi
90. sbcnel12g
91. sbcne12
92. sbcel1g
93. sbceq1g
94. sbcel2
95. sbceq2g
96. csbcom
97. sbcnestgfw
98. csbnestgfw
99. sbcnestgw
100. csbnestgw
101. sbcco3gw
102. sbcnestgf
103. csbnestgf
104. sbcnestg
105. csbnestg
106. sbcco3g
107. csbco3g
108. csbnest1g
109. csbidm
110. csbvarg
111. csbvargi
112. sbccsb
113. sbccsb2
114. rspcsbela
115. sbnfc2
116. csbab
117. csbun
118. csbin
119. csbie2df
120. 2nreu
121. un00
122. vss
123. 0pss
124. npss0
125. pssv
126. disj
127. disjOLD
128. disjr
129. disj1
130. reldisj
131. reldisjOLD
132. disj3
133. disjne
134. disjeq0
135. disjel
136. disj2
137. disj4
138. ssdisj
139. disjpss
140. undisj1
141. undisj2
142. ssindif0
143. inelcm
144. minel
145. undif4
146. disjssun
147. vdif0
148. difrab0eq
149. pssnel
150. disjdif
151. disjdifr
152. difin0
153. unvdif
154. undif1
155. undif2
156. undifabs
157. inundif
158. disjdif2
159. difun2
160. undif
161. ssdifin0
162. ssdifeq0
163. ssundif
164. difcom
165. pssdifcom1
166. pssdifcom2
167. difdifdir
168. uneqdifeq
169. raldifeq
170. r19.2z
171. r19.2zb
172. r19.3rz
173. r19.28z
174. r19.3rzv
175. r19.9rzv
176. r19.28zv
177. r19.37zv
178. r19.45zv
179. r19.44zv
180. r19.27z
181. r19.27zv
182. r19.36zv
183. ralidmw
184. rzal
185. rzalALT
186. rexn0
187. ralidm
188. ral0
189. ralf0
190. rexn0OLD
191. ralidmOLD
192. ral0OLD
193. ralf0OLD
194. ralnralall
195. falseral0
196. raaan
197. raaanv
198. sbss
199. sbcssg
200. raaan2
201. 2reu4lem
202. 2reu4
The conditional operator for classes
1. cif
2. df-if
3. dfif2
4. dfif6
5. ifeq1
6. ifeq2
7. iftrue
8. iftruei
9. iftrued
10. iffalse
11. iffalsei
12. iffalsed
13. ifnefalse
14. ifsb
15. dfif3
16. dfif4
17. dfif5
18. ifssun
19. ifeq12
20. ifeq1d
21. ifeq2d
22. ifeq12d
23. ifbi
24. ifbid
25. ifbieq1d
26. ifbieq2i
27. ifbieq2d
28. ifbieq12i
29. ifbieq12d
30. nfifd
31. nfif
32. ifeq1da
33. ifeq2da
34. ifeq12da
35. ifbieq12d2
36. ifclda
37. ifeqda
38. elimif
39. ifbothda
40. ifboth
41. ifid
42. eqif
43. ifval
44. elif
45. ifel
46. ifcl
47. ifcld
48. ifcli
49. ifexd
50. ifexg
51. ifex
52. ifeqor
53. ifnot
54. ifan
55. ifor
56. 2if2
57. ifcomnan
58. csbif
The weak deduction theorem for set theory
1. dedth
2. dedth2h
3. dedth3h
4. dedth4h
5. dedth2v
6. dedth3v
7. dedth4v
8. elimhyp
9. elimhyp2v
10. elimhyp3v
11. elimhyp4v
12. elimel
13. elimdhyp
14. keephyp
15. keephyp2v
16. keephyp3v
Power classes
1. cpw
2. pwjust
3. df-pw
4. elpwg
5. elpw
6. velpw
7. elpwOLD
8. elpwgOLD
9. elpwd
10. elpwi
11. elpwb
12. elpwid
13. elelpwi
14. sspw
15. sspwi
16. sspwd
17. pweq
18. pweqALT
19. pweqi
20. pweqd
21. pwunss
22. nfpw
23. pwidg
24. pwidb
25. pwid
26. pwss
27. pwundif
Unordered and ordered pairs
1. snjust
2. csn
3. df-sn
4. cpr
5. df-pr
6. ctp
7. df-tp
8. cop
9. df-op
10. cotp
11. df-ot
12. sneq
13. sneqi
14. sneqd
15. dfsn2
16. elsng
17. elsn
18. velsn
19. elsni
20. absn
21. dfpr2
22. dfsn2ALT
23. elprg
24. elpri
25. elpr
26. elpr2g
27. elpr2
28. elpr2OLD
29. nelpr2
30. nelpr1
31. nelpri
32. prneli
33. nelprd
34. eldifpr
35. rexdifpr
36. snidg
37. snidb
38. snid
39. vsnid
40. elsn2g
41. elsn2
42. nelsn
43. rabeqsn
44. rabsssn
45. ralsnsg
46. rexsns
47. rexsngf
48. ralsngf
49. reusngf
50. ralsng
51. rexsng
52. reusng
53. 2ralsng
54. ralsngOLD
55. rexsngOLD
56. rexreusng
57. exsnrex
58. ralsn
59. rexsn
60. elpwunsn
61. eqoreldif
62. eltpg
63. eldiftp
64. eltpi
65. eltp
66. dftp2
67. nfpr
68. ifpr
69. ralprgf
70. rexprgf
71. ralprg
72. ralprgOLD
73. rexprg
74. rexprgOLD
75. raltpg
76. rextpg
77. ralpr
78. rexpr
79. reuprg0
80. reuprg
81. reurexprg
82. raltp
83. rextp
84. nfsn
85. csbsng
86. csbprg
87. elinsn
88. disjsn
89. disjsn2
90. disjpr2
91. disjprsn
92. disjtpsn
93. disjtp2
94. snprc
95. snnzb
96. rmosn
97. r19.12sn
98. rabsn
99. rabsnifsb
100. rabsnif
101. rabrsn
102. euabsn2
103. euabsn
104. reusn
105. absneu
106. rabsneu
107. eusn
108. rabsnt
109. prcom
110. preq1
111. preq2
112. preq12
113. preq1i
114. preq2i
115. preq12i
116. preq1d
117. preq2d
118. preq12d
119. tpeq1
120. tpeq2
121. tpeq3
122. tpeq1d
123. tpeq2d
124. tpeq3d
125. tpeq123d
126. tprot
127. tpcoma
128. tpcomb
129. tpass
130. qdass
131. qdassr
132. tpidm12
133. tpidm13
134. tpidm23
135. tpidm
136. tppreq3
137. prid1g
138. prid2g
139. prid1
140. prid2
141. ifpprsnss
142. prprc1
143. prprc2
144. prprc
145. tpid1
146. tpid1g
147. tpid2
148. tpid2g
149. tpid3g
150. tpid3
151. snnzg
152. snn0d
153. snnz
154. prnz
155. prnzg
156. tpnz
157. tpnzd
158. raltpd
159. snssg
160. snss
161. eldifsn
162. ssdifsn
163. elpwdifsn
164. eldifsni
165. eldifsnneq
166. neldifsn
167. neldifsnd
168. rexdifsn
169. raldifsni
170. raldifsnb
171. eldifvsn
172. difsn
173. difprsnss
174. difprsn1
175. difprsn2
176. diftpsn3
177. difpr
178. tpprceq3
179. tppreqb
180. difsnb
181. difsnpss
182. snssi
183. snssd
184. difsnid
185. eldifeldifsn
186. pw0
187. pwpw0
188. snsspr1
189. snsspr2
190. snsstp1
191. snsstp2
192. snsstp3
193. prssg
194. prss
195. prssi
196. prssd
197. prsspwg
198. ssprss
199. ssprsseq
200. sssn
201. ssunsn2
202. ssunsn
203. eqsn
204. issn
205. n0snor2el
206. ssunpr
207. sspr
208. sstp
209. tpss
210. tpssi
211. sneqrg
212. sneqr
213. snsssn
214. mosneq
215. sneqbg
216. snsspw
217. prsspw
218. preq1b
219. preq2b
220. preqr1
221. preqr2
222. preq12b
223. opthpr
224. preqr1g
225. preq12bg
226. prneimg
227. prnebg
228. pr1eqbg
229. pr1nebg
230. preqsnd
231. prnesn
232. prneprprc
233. preqsn
234. preq12nebg
235. prel12g
236. opthprneg
237. elpreqprlem
238. elpreqpr
239. elpreqprb
240. elpr2elpr
241. dfopif
242. dfopifOLD
243. dfopg
244. dfop
245. opeq1
246. opeq1OLD
247. opeq2
248. opeq2OLD
249. opeq12
250. opeq1i
251. opeq2i
252. opeq12i
253. opeq1d
254. opeq2d
255. opeq12d
256. oteq1
257. oteq2
258. oteq3
259. oteq1d
260. oteq2d
261. oteq3d
262. oteq123d
263. nfop
264. nfopd
265. csbopg
266. opidg
267. opid
268. ralunsn
269. 2ralunsn
270. opprc
271. opprc1
272. opprc2
273. oprcl
274. pwsn
275. pwsnOLD
276. pwpr
277. pwtp
278. pwpwpw0
279. pwv
280. prproe
281. 3elpr2eq
The union of a class
1. cuni
2. df-uni
3. dfuni2
4. eluni
5. eluni2
6. elunii
7. nfunid
8. nfuni
9. uniss
10. unissi
11. unissd
12. unieq
13. unieqOLD
14. unieqi
15. unieqd
16. eluniab
17. elunirab
18. uniprg
19. unipr
20. uniprOLD
21. uniprgOLD
22. unisng
23. unisn
24. unisn3
25. dfnfc2
26. uniun
27. uniin
28. ssuni
29. uni0b
30. uni0c
31. uni0
32. csbuni
33. elssuni
34. unissel
35. unissb
36. uniss2
37. unidif
38. ssunieq
39. unimax
40. pwuni
The intersection of a class
1. cint
2. df-int
3. dfint2
4. inteq
5. inteqi
6. inteqd
7. elint
8. elint2
9. elintg
10. elinti
11. nfint
12. elintab
13. elintrab
14. elintrabg
15. int0
16. intss1
17. ssint
18. ssintab
19. ssintub
20. ssmin
21. intmin
22. intss
23. intssuni
24. ssintrab
25. unissint
26. intssuni2
27. intminss
28. intmin2
29. intmin3
30. intmin4
31. intab
32. int0el
33. intun
34. intprg
35. intpr
36. intprOLD
37. intprgOLD
38. intsng
39. intsn
40. uniintsn
41. uniintab
42. intunsn
43. rint0
44. elrint
45. elrint2
Indexed union and intersection
1. ciun
2. ciin
3. df-iun
4. df-iin
5. eliun
6. eliin
7. eliuni
8. iuncom
9. iuncom4
10. iunconst
11. iinconst
12. iuneqconst
13. iuniin
14. iinssiun
15. iunss1
16. iinss1
17. iuneq1
18. iineq1
19. ss2iun
20. iuneq2
21. iineq2
22. iuneq2i
23. iineq2i
24. iineq2d
25. iuneq2dv
26. iineq2dv
27. iuneq12df
28. iuneq1d
29. iuneq12d
30. iuneq2d
31. nfiun
32. nfiin
33. nfiung
34. nfiing
35. nfiu1
36. nfii1
37. dfiun2g
38. dfiin2g
39. dfiun2
40. dfiin2
41. dfiunv2
42. cbviun
43. cbviin
44. cbviung
45. cbviing
46. cbviunv
47. cbviinv
48. cbviunvg
49. cbviinvg
50. iunssf
51. iunss
52. ssiun
53. ssiun2
54. ssiun2s
55. iunss2
56. iunssd
57. iunab
58. iunrab
59. iunxdif2
60. ssiinf
61. ssiin
62. iinss
63. iinss2
64. uniiun
65. intiin
66. iunid
67. iun0
68. 0iun
69. 0iin
70. viin
71. iunsn
72. iunn0
73. iinab
74. iinrab
75. iinrab2
76. iunin2
77. iunin1
78. iinun2
79. iundif2
80. iindif1
81. 2iunin
82. iindif2
83. iinin2
84. iinin1
85. iinvdif
86. elriin
87. riin0
88. riinn0
89. riinrab
90. symdif0
91. symdifv
92. symdifid
93. iinxsng
94. iinxprg
95. iunxsng
96. iunxsn
97. iunxsngf
98. iunun
99. iunxun
100. iunxdif3
101. iunxprg
102. iunxiun
103. iinuni
104. iununi
105. sspwuni
106. pwssb
107. elpwpw
108. pwpwab
109. pwpwssunieq
110. elpwuni
111. iinpw
112. iunpwss
113. intss2
114. rintn0
Disjointness
1. wdisj
2. df-disj
3. dfdisj2
4. disjss2
5. disjeq2
6. disjeq2dv
7. disjss1
8. disjeq1
9. disjeq1d
10. disjeq12d
11. cbvdisj
12. cbvdisjv
13. nfdisjw
14. nfdisj
15. nfdisj1
16. disjor
17. disjors
18. disji2
19. disji
20. invdisj
21. invdisjrabw
22. invdisjrab
23. disjiun
24. disjord
25. disjiunb
26. disjiund
27. sndisj
28. 0disj
29. disjxsn
30. disjx0
31. disjprgw
32. disjprg
33. disjxiun
34. disjxun
35. disjss3
Binary relations
1. wbr
2. df-br
3. breq
4. breq1
5. breq2
6. breq12
7. breqi
8. breq1i
9. breq2i
10. breq12i
11. breq1d
12. breqd
13. breq2d
14. breq12d
15. breq123d
16. breqdi
17. breqan12d
18. breqan12rd
19. eqnbrtrd
20. nbrne1
21. nbrne2
22. eqbrtri
23. eqbrtrd
24. eqbrtrri
25. eqbrtrrd
26. breqtri
27. breqtrd
28. breqtrri
29. breqtrrd
30. 3brtr3i
31. 3brtr4i
32. 3brtr3d
33. 3brtr4d
34. 3brtr3g
35. 3brtr4g
36. eqbrtrid
37. eqbrtrrid
38. breqtrid
39. breqtrrid
40. eqbrtrdi
41. eqbrtrrdi
42. breqtrdi
43. breqtrrdi
44. ssbrd
45. ssbr
46. ssbri
47. nfbrd
48. nfbr
49. brab1
50. br0
51. brne0
52. brun
53. brin
54. brdif
55. sbcbr123
56. sbcbr
57. sbcbr12g
58. sbcbr1g
59. sbcbr2g
60. brsymdif
61. brralrspcev
62. brimralrspcev
Ordered-pair class abstractions (class builders)
1. copab
2. df-opab
3. opabss
4. opabbid
5. opabbidv
6. opabbii
7. nfopab
8. nfopab1
9. nfopab2
10. cbvopab
11. cbvopabv
12. cbvopab1
13. cbvopab1g
14. cbvopab2
15. cbvopab1s
16. cbvopab1v
17. cbvopab2v
18. unopab
Functions in maps-to notation
1. cmpt
2. df-mpt
3. mpteq12df
4. mpteq12f
5. mpteq12dva
6. mpteq12dv
7. mpteq12dvOLD
8. mpteq12
9. mpteq1
10. mpteq1d
11. mpteq1i
12. mpteq2ia
13. mpteq2i
14. mpteq12i
15. mpteq2da
16. mpteq2dva
17. mpteq2dv
18. nfmpt
19. nfmpt1
20. cbvmptf
21. cbvmptfg
22. cbvmpt
23. cbvmptg
24. cbvmptv
25. cbvmptvg
26. mptv
Transitive classes
1. wtr
2. df-tr
3. dftr2
4. dftr5
5. dftr3
6. dftr4
7. treq
8. trel
9. trel3
10. trss
11. trin
12. tr0
13. trv
14. triun
15. truni
16. triin
17. trint
18. trintss