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. drnfc2
42. nfabdw
43. nfabd
44. nfabd2
45. dvelimdc
46. dvelimc
47. nfcvf
48. nfcvf2
49. cleqf
50. abid2f
51. abeq2f
52. 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. nfrald
84. nfralw
85. nfral
86. nfra2w
87. nfra2
88. rgen2a
89. ralbida
90. ralbid
91. 2ralbida
92. raleqbii
93. ralcom4
94. ralnex
95. dfral2
96. rexnal
97. dfrex2
98. rexex
99. rexim
100. rexbi
101. reximia
102. reximi
103. reximi2
104. rexbii2
105. rexbiia
106. rexbii
107. 2rexbii
108. rexcom4
109. 2ex2rexrot
110. rexcom4a
111. rexanid
112. r19.29
113. r19.29r
114. r19.29imd
115. rexnal2
116. rexnal3
117. ralnex2
118. ralnex3
119. ralinexa
120. rexanali
121. nrexralim
122. risset
123. nelb
124. nrex
125. nrexdv
126. reximdv2
127. reximdvai
128. reximdv
129. reximdva
130. reximddv
131. reximssdv
132. reximdvva
133. reximddv2
134. r19.23v
135. rexlimiv
136. rexlimiva
137. rexlimivw
138. rexlimdv
139. rexlimdva
140. rexlimdvaa
141. rexlimdv3a
142. rexlimdva2
143. r19.29an
144. r19.29a
145. rexlimdvw
146. rexlimddv
147. rexlimivv
148. rexlimdvv
149. rexlimdvva
150. rexbidv2
151. rexbidva
152. rexbidv
153. 2rexbiia
154. 2rexbidva
155. 2rexbidv
156. rexralbidv
157. r2exlem
158. r2ex
159. rspe
160. rsp2e
161. nfre1
162. nfrexd
163. nfrexdg
164. nfrex
165. nfrexg
166. reximdai
167. reximd2a
168. r19.23t
169. r19.23
170. rexlimi
171. rexlimd2
172. rexlimd
173. rexbida
174. rexbidvaALT
175. rexbid
176. rexbidvALT
177. ralrexbid
178. ralrexbidOLD
179. r19.12
180. r2exf
181. rexeqbii
182. reuanid
183. rmoanid
184. r19.29af2
185. r19.29af
186. 2r19.29
187. r19.29d2r
188. r19.29vva
189. r19.30
190. r19.32v
191. r19.35
192. r19.36v
193. r19.37
194. r19.37v
195. r19.40
196. r19.41v
197. r19.41
198. r19.41vv
199. r19.42v
200. r19.43
201. r19.44v
202. r19.45v
203. ralcom
204. rexcom
205. rexcomOLD
206. ralcomf
207. rexcomf
208. ralcom13
209. rexcom13
210. ralrot3
211. rexrot4
212. ralcom2
213. ralcom3
214. reeanlem
215. reean
216. reeanv
217. 3reeanv
218. 2ralor
219. nfreu1
220. nfrmo1
221. nfreud
222. nfrmod
223. nfreuw
224. nfrmow
225. nfreu
226. nfrmo
227. rabid
228. rabrab
229. rabidim1
230. rabid2
231. rabid2f
232. rabbi
233. nfrab1
234. nfrabw
235. nfrab
236. reubida
237. reubidva
238. reubidv
239. reubiia
240. reubii
241. rmobida
242. rmobidva
243. rmobidv
244. rmobiia
245. rmobii
246. raleqf
247. rexeqf
248. reueq1f
249. rmoeq1f
250. raleqbidv
251. rexeqbidv
252. raleqbi1dv
253. rexeqbi1dv
254. raleq
255. rexeq
256. reueq1
257. rmoeq1
258. raleqi
259. rexeqi
260. raleqdv
261. rexeqdv
262. reueqd
263. rmoeqd
264. raleqbid
265. rexeqbid
266. raleqbidva
267. rexeqbidva
268. raleleq
269. raleleqALT
270. mormo
271. reu5
272. reurex
273. 2reu2rex
274. reurmo
275. rmo5
276. nrexrmo
277. reueubd
278. cbvralfw
279. cbvralfwOLD
280. cbvrexfw
281. cbvralf
282. cbvrexf
283. cbvralw
284. cbvrexw
285. cbvreuw
286. cbvrmow
287. cbvrmowOLD
288. cbvral
289. cbvrex
290. cbvreu
291. cbvrmo
292. cbvralvw
293. cbvrexvw
294. cbvreuvw
295. cbvralv
296. cbvrexv
297. cbvreuv
298. cbvrmov
299. cbvraldva2
300. cbvrexdva2
301. cbvrexdva2OLD
302. cbvraldva
303. cbvrexdva
304. cbvral2vw
305. cbvrex2vw
306. cbvral3vw
307. cbvral2v
308. cbvrex2v
309. cbvral3v
310. cbvralsvw
311. cbvrexsvw
312. cbvralsv
313. cbvrexsv
314. sbralie
315. rabbiia
316. rabbii
317. rabbida
318. rabbid
319. rabbidva2
320. rabbia2
321. rabbidva
322. rabbidvaOLD
323. rabbidv
324. rabeqf
325. rabeqi
326. rabeqiOLD
327. rabeq
328. rabeqdv
329. rabeqbidv
330. rabeqbidva
331. rabeq2i
332. rabswap
333. cbvrabw
334. cbvrab
335. cbvrabv
336. rabrabi
337. rabeqcda
338. ralrimia
339. 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. issetiOLD
18. issetri
19. eqvisset
20. elex
21. elexi
22. elexd
23. elissetOLD
24. elex2
25. elex22
26. prcnel
27. ralv
28. rexv
29. reuv
30. rmov
31. rabab
32. rexcom4b
33. ralcom4OLD
34. rexcom4OLD
35. ceqsalt
36. ceqsralt
37. ceqsalg
38. ceqsalgALT
39. ceqsal
40. ceqsalv
41. ceqsralv
42. gencl
43. 2gencl
44. 3gencl
45. cgsexg
46. cgsex2g
47. cgsex4g
48. cgsex4gOLD
49. ceqsex
50. ceqsexv
51. ceqsexv2d
52. ceqsex2
53. ceqsex2v
54. ceqsex3v
55. ceqsex4v
56. ceqsex6v
57. ceqsex8v
58. gencbvex
59. gencbvex2
60. gencbval
61. sbhypf
62. vtoclgft
63. vtoclgftOLD
64. vtocldf
65. vtocld
66. vtocldOLD
67. vtocl2d
68. vtoclf
69. vtocl
70. vtoclALT
71. vtocl2
72. vtocl2OLD
73. vtocl3
74. vtoclb
75. vtoclgf
76. vtoclg1f
77. vtoclg
78. vtoclgOLD
79. vtoclbg
80. vtocl2gf
81. vtocl3gf
82. vtocl2g
83. vtoclgaf
84. vtoclga
85. vtocl2ga
86. vtocl2gaf
87. vtocl3gaf
88. vtocl3ga
89. vtocl4g
90. vtocl4ga
91. vtocleg
92. vtoclegft
93. vtoclef
94. vtocle
95. vtoclri
96. spcimgft
97. spcgft
98. spcimgf
99. spcimegf
100. spcgf
101. spcegf
102. spcimdv
103. spcdv
104. spcimedv
105. spcgv
106. spcgvOLD
107. spcegv
108. spcegvOLD
109. spcedv
110. spc2egv
111. spc2gv
112. spc2ed
113. spc2d
114. spc3egv
115. spc3gv
116. spcv
117. spcev
118. spc2ev
119. rspct
120. rspcdf
121. rspc
122. rspce
123. rspcimdv
124. rspcimedv
125. rspcdv
126. rspcedv
127. rspcebdv
128. rspcv
129. rspcvOLD
130. rspccv
131. rspcva
132. rspccva
133. rspcev
134. rspcevOLD
135. rspcdva
136. rspcedvd
137. rspcime
138. rspceaimv
139. rspcedeq1vd
140. rspcedeq2vd
141. rspc2
142. rspc2gv
143. rspc2v
144. rspc2va
145. rspc2ev
146. rspc3v
147. rspc3ev
148. rspceeqv
149. ralxpxfr2d
150. rexraleqim
151. eqvincg
152. eqvinc
153. eqvincf
154. alexeqg
155. ceqex
156. ceqsexg
157. ceqsexgv
158. ceqsexgvOLD
159. ceqsrexv
160. ceqsrexbv
161. ceqsrex2v
162. clel2g
163. clel2gOLD
164. clel2
165. clel3g
166. clel3
167. clel4g
168. clel4
169. clel4OLD
170. clel5
171. pm13.183
172. rr19.3v
173. rr19.28v
174. elabgt
175. elabgf
176. elabf
177. elabgw
178. elab2gw
179. elabg
180. elab
181. elab2g
182. elabd
183. elab2
184. elab4g
185. elab3gf
186. elab3g
187. elab3
188. elrabi
189. elrabiOLD
190. elrabf
191. rabtru
192. rabeqc
193. elrab3t
194. elrab
195. elrab3
196. elrabd
197. elrab2
198. elrab2w
199. ralab
200. ralrab
201. rexab
202. rexrab
203. ralab2
204. ralab2OLD
205. ralrab2
206. rexab2
207. rexab2OLD
208. rexrab2
209. abidnf
210. dedhb
211. nelrdva
212. eqeu
213. moeq
214. eueq
215. eueqi
216. eueq2
217. eueq3
218. moeq3
219. mosub
220. mo2icl
221. mob2
222. moi2
223. mob
224. moi
225. morex
226. euxfr2w
227. euxfrw
228. euxfr2
229. euxfr
230. euind
231. reu2
232. reu6
233. reu3
234. reu6i
235. eqreu
236. rmo4
237. reu4
238. reu7
239. reu8
240. rmo3f
241. rmo4f
242. reu2eqd
243. reueq
244. rmoeq
245. rmoan
246. rmoim
247. rmoimia
248. rmoimi
249. rmoimi2
250. 2reu5a
251. reuimrmo
252. 2reuswap
253. 2reuswap2
254. reuxfrd
255. reuxfr
256. reuxfr1d
257. reuxfr1ds
258. reuxfr1
259. reuind
260. 2rmorex
261. 2reu5lem1
262. 2reu5lem2
263. 2reu5lem3
264. 2reu5
265. 2reurex
266. 2reurmo
267. 2rmoswap
268. 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. dfnul2
4. dfnul3
5. dfnul4
6. noel
7. nel02
8. n0i
9. ne0i
10. ne0d
11. n0ii
12. ne0ii
13. vn0
14. vn0ALT
15. eq0f
16. neq0f
17. n0f
18. eq0
19. eq0ALT
20. neq0
21. n0
22. eq0OLDOLD
23. neq0OLD
24. n0OLD
25. nel0
26. reximdva0
27. rspn0
28. rspn0OLD
29. n0rex
30. ssn0rex
31. n0moeu
32. rex0
33. reu0
34. rmo0
35. 0el
36. n0el
37. eqeuel
38. ssdif0
39. difn0
40. pssdifn0
41. pssdif
42. ndisj
43. difin0ss
44. inssdif0
45. difid
46. difidALT
47. dif0
48. ab0
49. ab0ALT
50. dfnf5
51. ab0orv
52. ab0orvALT
53. abn0
54. abn0OLD
55. rab0
56. rabeq0
57. rabn0
58. rabxm
59. rabnc
60. elneldisj
61. elnelun
62. un0
63. in0
64. 0un
65. 0in
66. inv1
67. unv
68. 0ss
69. ss0b
70. ss0
71. sseq0
72. ssn0
73. 0dif
74. abf
75. abfOLD
76. eq0rdv
77. eq0rdvALT
78. csbprc
79. csb0
80. csb0OLD
81. sbcel12
82. sbceqg
83. sbceqi
84. sbcnel12g
85. sbcne12
86. sbcel1g
87. sbceq1g
88. sbcel2
89. sbceq2g
90. csbcom
91. sbcnestgfw
92. csbnestgfw
93. sbcnestgw
94. csbnestgw
95. sbcco3gw
96. sbcnestgf
97. csbnestgf
98. sbcnestg
99. csbnestg
100. sbcco3g
101. csbco3g
102. csbnest1g
103. csbidm
104. csbvarg
105. csbvargi
106. sbccsb
107. sbccsb2
108. rspcsbela
109. sbnfc2
110. csbab
111. csbun
112. csbin
113. csbie2df
114. 2nreu
115. un00
116. vss
117. 0pss
118. npss0
119. pssv
120. disj
121. disjOLD
122. disjr
123. disj1
124. reldisj
125. reldisjOLD
126. disj3
127. disjne
128. disjeq0
129. disjel
130. disj2
131. disj4
132. ssdisj
133. disjpss
134. undisj1
135. undisj2
136. ssindif0
137. inelcm
138. minel
139. undif4
140. disjssun
141. vdif0
142. difrab0eq
143. pssnel
144. disjdif
145. disjdifr
146. difin0
147. unvdif
148. undif1
149. undif2
150. undifabs
151. inundif
152. disjdif2
153. difun2
154. undif
155. ssdifin0
156. ssdifeq0
157. ssundif
158. difcom
159. pssdifcom1
160. pssdifcom2
161. difdifdir
162. uneqdifeq
163. raldifeq
164. r19.2z
165. r19.2zb
166. r19.3rz
167. r19.28z
168. r19.3rzv
169. r19.9rzv
170. r19.28zv
171. r19.37zv
172. r19.45zv
173. r19.44zv
174. r19.27z
175. r19.27zv
176. r19.36zv
177. rzal
178. rzalALT
179. rexn0
180. ralidm
181. ral0
182. ralf0
183. rexn0OLD
184. ralidmOLD
185. ral0OLD
186. ralf0OLD
187. ralnralall
188. falseral0
189. raaan
190. raaanv
191. sbss
192. sbcssg
193. raaan2
194. 2reu4lem
195. 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. rexreusng
55. exsnrex
56. ralsn
57. rexsn
58. elpwunsn
59. eqoreldif
60. eltpg
61. eldiftp
62. eltpi
63. eltp
64. dftp2
65. nfpr
66. ifpr
67. ralprgf
68. rexprgf
69. ralprg
70. rexprg
71. raltpg
72. rextpg
73. ralpr
74. rexpr
75. reuprg0
76. reuprg
77. reurexprg
78. raltp
79. rextp
80. nfsn
81. csbsng
82. csbprg
83. elinsn
84. disjsn
85. disjsn2
86. disjpr2
87. disjprsn
88. disjtpsn
89. disjtp2
90. snprc
91. snnzb
92. rmosn
93. r19.12sn
94. rabsn
95. rabsnifsb
96. rabsnif
97. rabrsn
98. euabsn2
99. euabsn
100. reusn
101. absneu
102. rabsneu
103. eusn
104. rabsnt
105. prcom
106. preq1
107. preq2
108. preq12
109. preq1i
110. preq2i
111. preq12i
112. preq1d
113. preq2d
114. preq12d
115. tpeq1
116. tpeq2
117. tpeq3
118. tpeq1d
119. tpeq2d
120. tpeq3d
121. tpeq123d
122. tprot
123. tpcoma
124. tpcomb
125. tpass
126. qdass
127. qdassr
128. tpidm12
129. tpidm13
130. tpidm23
131. tpidm
132. tppreq3
133. prid1g
134. prid2g
135. prid1
136. prid2
137. ifpprsnss
138. prprc1
139. prprc2
140. prprc
141. tpid1
142. tpid1g
143. tpid2
144. tpid2g
145. tpid3g
146. tpid3
147. snnzg
148. snn0d
149. snnz
150. prnz
151. prnzg
152. tpnz
153. tpnzd
154. raltpd
155. snssg
156. snss
157. eldifsn
158. ssdifsn
159. elpwdifsn
160. eldifsni
161. eldifsnneq
162. neldifsn
163. neldifsnd
164. rexdifsn
165. raldifsni
166. raldifsnb
167. eldifvsn
168. difsn
169. difprsnss
170. difprsn1
171. difprsn2
172. diftpsn3
173. difpr
174. tpprceq3
175. tppreqb
176. difsnb
177. difsnpss
178. snssi
179. snssd
180. difsnid
181. eldifeldifsn
182. pw0
183. pwpw0
184. snsspr1
185. snsspr2
186. snsstp1
187. snsstp2
188. snsstp3
189. prssg
190. prss
191. prssi
192. prssd
193. prsspwg
194. ssprss
195. ssprsseq
196. sssn
197. ssunsn2
198. ssunsn
199. eqsn
200. issn
201. n0snor2el
202. ssunpr
203. sspr
204. sstp
205. tpss
206. tpssi
207. sneqrg
208. sneqr
209. snsssn
210. mosneq
211. sneqbg
212. snsspw
213. prsspw
214. preq1b
215. preq2b
216. preqr1
217. preqr2
218. preq12b
219. opthpr
220. preqr1g
221. preq12bg
222. prneimg
223. prnebg
224. pr1eqbg
225. pr1nebg
226. preqsnd
227. prnesn
228. prneprprc
229. preqsn
230. preq12nebg
231. prel12g
232. opthprneg
233. elpreqprlem
234. elpreqpr
235. elpreqprb
236. elpr2elpr
237. dfopif
238. dfopifOLD
239. dfopg
240. dfop
241. opeq1
242. opeq1OLD
243. opeq2
244. opeq2OLD
245. opeq12
246. opeq1i
247. opeq2i
248. opeq12i
249. opeq1d
250. opeq2d
251. opeq12d
252. oteq1
253. oteq2
254. oteq3
255. oteq1d
256. oteq2d
257. oteq3d
258. oteq123d
259. nfop
260. nfopd
261. csbopg
262. opidg
263. opid
264. ralunsn
265. 2ralunsn
266. opprc
267. opprc1
268. opprc2
269. oprcl
270. pwsn
271. pwsnOLD
272. pwpr
273. pwtp
274. pwpwpw0
275. pwv
276. prproe
277. 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. dfiun2gOLD
39. dfiin2g
40. dfiun2
41. dfiin2
42. dfiunv2
43. cbviun
44. cbviin
45. cbviung
46. cbviing
47. cbviunv
48. cbviinv
49. cbviunvg
50. cbviinvg
51. iunssf
52. iunss
53. ssiun
54. ssiun2
55. ssiun2s
56. iunss2
57. iunssd
58. iunab
59. iunrab
60. iunxdif2
61. ssiinf
62. ssiin
63. iinss
64. iinss2
65. uniiun
66. intiin
67. iunid
68. iun0
69. 0iun
70. 0iin
71. viin
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