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. nfcriv
8. nfcd
9. nfcrd
10. nfcrii
11. nfcri
12. nfceqdf
13. nfceqi
14. nfceqiOLD
15. nfcxfr
16. nfcxfrd
17. nfcv
18. nfcvd
19. nfab1
20. nfnfc1
21. clelsb3fw
22. clelsb3f
23. clelsb3fOLD
24. nfab
25. nfabg
26. nfaba1
27. nfaba1g
28. nfeqd
29. nfeld
30. nfnfc
31. nfeq
32. nfel
33. nfeq1
34. nfel1
35. nfeq2
36. nfel2
37. drnfc1
38. drnfc1OLD
39. drnfc2
40. nfabdw
41. nfabd
42. nfabd2
43. nfabd2OLD
44. nfabdOLD
45. dvelimdc
46. dvelimc
47. nfcvf
48. nfcvf2
49. nfcvfOLD
50. cleqf
51. cleqfOLD
52. abid2f
53. abeq2f
54. abeq2fOLD
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. ralanidOLD
33. r19.26
34. r19.26-2
35. r19.26-3
36. r19.26m
37. ralbiim
38. r19.21v
39. ralimdv2
40. ralimdva
41. ralimdv
42. ralimdvva
43. hbralrimi
44. ralrimiv
45. ralrimiva
46. ralrimivw
47. r19.27v
48. r19.27vOLD
49. r19.28v
50. r19.28vOLD
51. ralrimdv
52. ralrimdva
53. ralrimivv
54. ralrimivva
55. ralrimivvva
56. ralrimdvv
57. ralrimdvva
58. ralbidv2
59. ralbidva
60. ralbidv
61. 2ralbidva
62. 2ralbidv
63. r2allem
64. r2al
65. r3al
66. rgen2
67. rgen3
68. rsp
69. rspa
70. rspec
71. r19.21bi
72. r19.21biOLD
73. r19.21be
74. rspec2
75. rspec3
76. rsp2
77. r19.21t
78. r19.21
79. ralrimi
80. ralimdaa
81. ralrimd
82. nfra1
83. hbra1
84. hbral
85. r2alf
86. nfraldw
87. nfrald
88. nfralw
89. nfral
90. nfra2w
91. nfra2
92. rgen2a
93. ralbida
94. ralbid
95. 2ralbida
96. ralbiOLD
97. raleqbii
98. ralcom4
99. ralnex
100. dfral2
101. rexnal
102. dfrex2
103. rexex
104. rexim
105. reximia
106. reximi
107. reximi2
108. rexbii2
109. rexbiia
110. rexbii
111. 2rexbii
112. rexcom4
113. 2ex2rexrot
114. rexcom4a
115. rexanid
116. rexanidOLD
117. r19.29
118. r19.29r
119. r19.29rOLD
120. r19.29imd
121. rexnal2
122. rexnal3
123. ralnex2
124. ralnex2OLD
125. ralnex3
126. ralnex3OLD
127. ralinexa
128. rexanali
129. nrexralim
130. risset
131. nelb
132. nrex
133. nrexdv
134. reximdv2
135. reximdvai
136. reximdv
137. reximdva
138. reximddv
139. reximssdv
140. reximdvva
141. reximddv2
142. r19.23v
143. rexlimiv
144. rexlimiva
145. rexlimivw
146. rexlimdv
147. rexlimdva
148. rexlimdvaa
149. rexlimdv3a
150. rexlimdva2
151. r19.29an
152. r19.29a
153. rexlimdvw
154. rexlimddv
155. rexlimivv
156. rexlimdvv
157. rexlimdvva
158. rexbidv2
159. rexbidva
160. rexbidv
161. 2rexbiia
162. 2rexbidva
163. 2rexbidv
164. rexralbidv
165. r2exlem
166. r2ex
167. rspe
168. rsp2e
169. nfre1
170. nfrexd
171. nfrexdg
172. nfrex
173. nfrexg
174. reximdai
175. reximd2a
176. r19.23t
177. r19.23
178. rexlimi
179. rexlimd2
180. rexlimd
181. rexbida
182. rexbidvaALT
183. rexbid
184. rexbidvALT
185. ralrexbid
186. ralrexbidOLD
187. r19.12
188. r2exf
189. rexeqbii
190. r19.12OLD
191. reuanid
192. rmoanid
193. r19.29af2
194. r19.29af
195. r19.29anOLD
196. r19.29aOLD
197. 2r19.29
198. r19.29d2r
199. r19.29vva
200. r19.29vvaOLD
201. r19.30
202. r19.30OLD
203. r19.32v
204. r19.35
205. r19.36v
206. r19.37
207. r19.37v
208. r19.37vOLD
209. r19.40
210. r19.41v
211. r19.41
212. r19.41vv
213. r19.42v
214. r19.43
215. r19.44v
216. r19.45v
217. ralcom
218. rexcom
219. rexcomOLD
220. ralcomf
221. rexcomf
222. ralcom13
223. rexcom13
224. ralrot3
225. rexrot4
226. ralcom2
227. ralcom3
228. reeanlem
229. reean
230. reeanv
231. 3reeanv
232. 2ralor
233. nfreu1
234. nfrmo1
235. nfreud
236. nfrmod
237. nfreuw
238. nfrmow
239. nfreu
240. nfrmo
241. rabid
242. rabrab
243. rabidim1
244. rabid2
245. rabid2f
246. rabbi
247. nfrab1
248. nfrabw
249. nfrab
250. reubida
251. reubidva
252. reubidv
253. reubiia
254. reubii
255. rmobida
256. rmobidva
257. rmobidv
258. rmobiia
259. rmobii
260. raleqf
261. rexeqf
262. reueq1f
263. rmoeq1f
264. raleqbidv
265. rexeqbidv
266. raleqbi1dv
267. rexeqbi1dv
268. raleq
269. rexeq
270. reueq1
271. rmoeq1
272. raleqOLD
273. rexeqOLD
274. reueq1OLD
275. rmoeq1OLD
276. raleqi
277. rexeqi
278. raleqdv
279. rexeqdv
280. raleqbi1dvOLD
281. rexeqbi1dvOLD
282. reueqd
283. rmoeqd
284. raleqbid
285. rexeqbid
286. raleqbidva
287. rexeqbidva
288. raleleq
289. raleleqALT
290. mormo
291. reu5
292. reurex
293. 2reu2rex
294. reurmo
295. rmo5
296. nrexrmo
297. reueubd
298. cbvralfw
299. cbvrexfw
300. cbvralf
301. cbvrexf
302. cbvralw
303. cbvrexw
304. cbvreuw
305. cbvrmow
306. cbvral
307. cbvrex
308. cbvreu
309. cbvrmo
310. cbvralvw
311. cbvrexvw
312. cbvreuvw
313. cbvralv
314. cbvrexv
315. cbvreuv
316. cbvrmov
317. cbvraldva2
318. cbvrexdva2
319. cbvrexdva2OLD
320. cbvraldva
321. cbvrexdva
322. cbvral2vw
323. cbvrex2vw
324. cbvral3vw
325. cbvral2v
326. cbvrex2v
327. cbvral3v
328. cbvralsvw
329. cbvrexsvw
330. cbvralsv
331. cbvrexsv
332. sbralie
333. rabbiia
334. rabbii
335. rabbida
336. rabbid
337. rabbidva2
338. rabbia2
339. rabbidva
340. rabbidvaOLD
341. rabbidv
342. rabeqf
343. rabeqi
344. rabeq
345. rabeqdv
346. rabeqbidv
347. rabeqbidva
348. rabeq2i
349. rabswap
350. cbvrabw
351. cbvrab
352. cbvrabv
353. cbvrabvOLD
354. rabrabi
The universal class
1. cvv
2. vjust
3. df-v
4. vex
5. vexOLD
6. elv
7. elvd
8. el2v
9. eqv
10. eqvf
11. abv
12. elisset
13. isset
14. issetf
15. isseti
16. issetiOLD
17. issetri
18. eqvisset
19. elex
20. elexi
21. elexd
22. elissetOLD
23. elex2
24. elex22
25. prcnel
26. ralv
27. rexv
28. reuv
29. rmov
30. rabab
31. rexcom4b
32. ralcom4OLD
33. rexcom4OLD
34. ceqsalt
35. ceqsralt
36. ceqsalg
37. ceqsalgALT
38. ceqsal
39. ceqsalv
40. ceqsralv
41. gencl
42. 2gencl
43. 3gencl
44. cgsexg
45. cgsex2g
46. cgsex4g
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. vtocl2d
65. vtoclf
66. vtocl
67. vtoclALT
68. vtocl2
69. vtocl2OLD
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. spcgvOLD
104. spcegv
105. spcegvOLD
106. spcedv
107. spc2egv
108. spc2gv
109. spc2ed
110. spc2d
111. spc3egv
112. spc3gv
113. spcv
114. spcev
115. spc2ev
116. rspct
117. rspcdf
118. rspc
119. rspce
120. rspcimdv
121. rspcimedv
122. rspcdv
123. rspcedv
124. rspcebdv
125. rspcv
126. rspcvOLD
127. rspccv
128. rspcva
129. rspccva
130. rspcev
131. rspcevOLD
132. rspcdva
133. rspcedvd
134. rspcime
135. rspceaimv
136. rspcedeq1vd
137. rspcedeq2vd
138. rspc2
139. rspc2gv
140. rspc2v
141. rspc2va
142. rspc2ev
143. rspc3v
144. rspc3ev
145. rspceeqv
146. ralxpxfr2d
147. rexraleqim
148. eqvincg
149. eqvinc
150. eqvincf
151. alexeqg
152. ceqex
153. ceqsexg
154. ceqsexgv
155. ceqsexgvOLD
156. ceqsrexv
157. ceqsrexbv
158. ceqsrex2v
159. clel2g
160. clel2
161. clel3g
162. clel3
163. clel4
164. clel5
165. clel5OLD
166. pm13.183
167. rr19.3v
168. rr19.28v
169. elabgt
170. elabgf
171. elabf
172. elabg
173. elab
174. elab2g
175. elabd
176. elab2
177. elab4g
178. elab3gf
179. elab3g
180. elab3
181. elrabi
182. elrabf
183. rabtru
184. rabeqc
185. elrab3t
186. elrab
187. elrab3
188. elrabd
189. elrab2
190. ralab
191. ralrab
192. rexab
193. rexrab
194. ralab2
195. ralab2OLD
196. ralrab2
197. rexab2
198. rexab2OLD
199. rexrab2
200. abidnf
201. dedhb
202. nelrdva
203. eqeu
204. moeq
205. eueq
206. eueqi
207. eueq2
208. eueq3
209. moeq3
210. mosub
211. mo2icl
212. mob2
213. moi2
214. mob
215. moi
216. morex
217. euxfr2w
218. euxfrw
219. euxfr2
220. euxfr
221. euind
222. reu2
223. reu6
224. reu3
225. reu6i
226. eqreu
227. rmo4
228. reu4
229. reu7
230. reu8
231. rmo3f
232. rmo4f
233. reu2eqd
234. reueq
235. rmoeq
236. rmoan
237. rmoim
238. rmoimia
239. rmoimi
240. rmoimi2
241. 2reu5a
242. reuimrmo
243. 2reuswap
244. 2reuswap2
245. reuxfrd
246. reuxfr
247. reuxfr1d
248. reuxfr1ds
249. reuxfr1
250. reuind
251. 2rmorex
252. 2reu5lem1
253. 2reu5lem2
254. 2reu5lem3
255. 2reu5
256. 2reurex
257. 2reurmo
258. 2rmoswap
259. 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. 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. sbc6g
31. sbc6
32. sbc7
33. cbvsbcw
34. cbvsbcvw
35. cbvsbc
36. cbvsbcv
37. sbciegft
38. sbciegf
39. sbcieg
40. sbcie2g
41. sbcie
42. sbciedf
43. sbcied
44. sbcied2
45. elrabsf
46. eqsbc3
47. sbcng
48. sbcimg
49. sbcan
50. sbcor
51. sbcbig
52. sbcn1
53. sbcim1
54. sbcbid
55. sbcbidv
56. sbcbidvOLD
57. sbcbii
58. sbcbi1
59. sbcbi2
60. sbcbi2OLD
61. sbcal
62. sbcex2
63. sbceqal
64. sbeqalb
65. eqsbc3r
66. sbc3an
67. sbcel1v
68. sbcel2gv
69. sbcel21v
70. sbcimdv
71. sbctt
72. sbcgf
73. sbc19.21g
74. sbcg
75. sbcgfi
76. sbc2iegf
77. sbc2ie
78. sbc2iedv
79. sbc3ie
80. sbccomlem
81. sbccom
82. sbcralt
83. sbcrext
84. sbcralg
85. sbcrex
86. sbcreu
87. reu8nf
88. sbcabel
89. rspsbc
90. rspsbca
91. rspesbca
92. spesbc
93. spesbcd
94. sbcth2
95. ra4v
96. ra4
97. rmo2
98. rmo2i
99. rmo3
100. rmob
101. rmoi
102. rmob2
103. rmoi2
104. rmoanim
105. rmoanimALT
106. reuan
107. 2reu1
108. 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
Subclasses and subsets
1. df-ss
2. dfss
3. df-pss
4. dfss2
5. dfss3
6. dfss6
7. dfss2f
8. dfss3f
9. nfss
10. ssel
11. ssel2
12. sseli
13. sselii
14. sseldi
15. sseld
16. sselda
17. sseldd
18. ssneld
19. ssneldd
20. ssriv
21. ssrd
22. ssrdv
23. sstr2
24. sstr
25. sstri
26. sstrd
27. sstrid
28. sstrdi
29. sylan9ss
30. sylan9ssr
31. eqss
32. eqssi
33. eqssd
34. sssseq
35. eqrd
36. eqri
37. eqelssd
38. ssid
39. ssidd
40. ssv
41. sseq1
42. sseq2
43. sseq12
44. sseq1i
45. sseq2i
46. sseq12i
47. sseq1d
48. sseq2d
49. sseq12d
50. eqsstri
51. eqsstrri
52. sseqtri
53. sseqtrri
54. eqsstrd
55. eqsstrrd
56. sseqtrd
57. sseqtrrd
58. 3sstr3i
59. 3sstr4i
60. 3sstr3g
61. 3sstr4g
62. 3sstr3d
63. 3sstr4d
64. eqsstrid
65. eqsstrrid
66. sseqtrdi
67. sseqtrrdi
68. sseqtrid
69. sseqtrrid
70. eqsstrdi
71. eqsstrrdi
72. eqimss
73. eqimss2
74. eqimssi
75. eqimss2i
76. nssne1
77. nssne2
78. nss
79. nelss
80. ssrexf
81. ssrmof
82. ssralv
83. ssrexv
84. ss2ralv
85. ss2rexv
86. ralss
87. rexss
88. ss2ab
89. abss
90. ssab
91. ssabral
92. ss2abi
93. ss2abdv
94. abssdv
95. abssi
96. ss2rab
97. rabss
98. ssrab
99. ssrabdv
100. rabssdv
101. ss2rabdv
102. ss2rabi
103. rabss2
104. ssab2
105. ssrab2
106. ssrab3
107. rabssrabd
108. ssrabeq
109. rabssab
110. uniiunlem
111. dfpss2
112. dfpss3
113. psseq1
114. psseq2
115. psseq1i
116. psseq2i
117. psseq12i
118. psseq1d
119. psseq2d
120. psseq12d
121. pssss
122. pssne
123. pssssd
124. pssned
125. sspss
126. pssirr
127. pssn2lp
128. sspsstri
129. ssnpss
130. psstr
131. sspsstr
132. psssstr
133. psstrd
134. sspsstrd
135. psssstrd
136. npss
137. ssnelpss
138. ssnelpssd
139. 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. dfnul2OLD
5. dfnul3
6. noel
7. noelOLD
8. nel02
9. n0i
10. ne0i
11. ne0d
12. n0ii
13. ne0ii
14. vn0
15. eq0f
16. neq0f
17. n0f
18. eq0
19. neq0
20. n0
21. nel0
22. reximdva0
23. rspn0
24. n0rex
25. ssn0rex
26. n0moeu
27. rex0
28. reu0
29. rmo0
30. 0el
31. n0el
32. eqeuel
33. ssdif0
34. difn0
35. pssdifn0
36. pssdif
37. ndisj
38. difin0ss
39. inssdif0
40. difid
41. difidALT
42. dif0
43. ab0
44. dfnf5
45. ab0orv
46. abn0
47. rab0
48. rabeq0
49. rabn0
50. rabxm
51. rabnc
52. elneldisj
53. elnelun
54. un0
55. in0
56. 0un
57. 0in
58. inv1
59. unv
60. 0ss
61. ss0b
62. ss0
63. sseq0
64. ssn0
65. 0dif
66. abf
67. eq0rdv
68. csbprc
69. csb0
70. sbcel12
71. sbceqg
72. sbceqi
73. sbcnel12g
74. sbcne12
75. sbcel1g
76. sbceq1g
77. sbcel2
78. sbceq2g
79. csbcom
80. sbcnestgfw
81. csbnestgfw
82. sbcnestgw
83. csbnestgw
84. sbcco3gw
85. sbcnestgf
86. csbnestgf
87. sbcnestg
88. csbnestg
89. sbcco3g
90. csbco3g
91. csbnest1g
92. csbidm
93. csbvarg
94. csbvargi
95. sbccsb
96. sbccsb2
97. rspcsbela
98. sbnfc2
99. csbab
100. csbun
101. csbin
102. csbie2df
103. 2nreu
104. un00
105. vss
106. 0pss
107. npss0
108. pssv
109. disj
110. disjr
111. disj1
112. reldisj
113. disj3
114. disjne
115. disjeq0
116. disjel
117. disj2
118. disj4
119. ssdisj
120. disjpss
121. undisj1
122. undisj2
123. ssindif0
124. inelcm
125. minel
126. undif4
127. disjssun
128. vdif0
129. difrab0eq
130. pssnel
131. disjdif
132. difin0
133. unvdif
134. undif1
135. undif2
136. undifabs
137. inundif
138. disjdif2
139. difun2
140. undif
141. ssdifin0
142. ssdifeq0
143. ssundif
144. difcom
145. pssdifcom1
146. pssdifcom2
147. difdifdir
148. uneqdifeq
149. raldifeq
150. r19.2z
151. r19.2zb
152. r19.3rz
153. r19.28z
154. r19.3rzv
155. r19.9rzv
156. r19.28zv
157. r19.37zv
158. r19.45zv
159. r19.44zv
160. r19.27z
161. r19.27zv
162. r19.36zv
163. rzal
164. rexn0
165. ralidm
166. ral0
167. ralf0
168. ralnralall
169. falseral0
170. raaan
171. raaanv
172. sbss
173. sbcssg
174. raaan2
175. 2reu4lem
176. 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. ifeq12
19. ifeq1d
20. ifeq2d
21. ifeq12d
22. ifbi
23. ifbid
24. ifbieq1d
25. ifbieq2i
26. ifbieq2d
27. ifbieq12i
28. ifbieq12d
29. nfifd
30. nfif
31. ifeq1da
32. ifeq2da
33. ifeq12da
34. ifbieq12d2
35. ifclda
36. ifeqda
37. elimif
38. ifbothda
39. ifboth
40. ifid
41. eqif
42. ifval
43. elif
44. ifel
45. ifcl
46. ifcld
47. ifcli
48. ifexg
49. ifex
50. ifeqor
51. ifnot
52. ifan
53. ifor
54. 2if2
55. ifcomnan
56. 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. elpr2
27. nelpr2
28. nelpr1
29. nelpri
30. prneli
31. nelprd
32. eldifpr
33. rexdifpr
34. snidg
35. snidb
36. snid
37. vsnid
38. elsn2g
39. elsn2
40. nelsn
41. rabeqsn
42. rabsssn
43. ralsnsg
44. rexsns
45. rexsngf
46. ralsngf
47. reusngf
48. ralsng
49. rexsng
50. reusng
51. 2ralsng
52. rexreusng
53. exsnrex
54. ralsn
55. rexsn
56. elpwunsn
57. eqoreldif
58. eltpg
59. eldiftp
60. eltpi
61. eltp
62. dftp2
63. nfpr
64. ifpr
65. ralprgf
66. rexprgf
67. ralprg
68. rexprg
69. raltpg
70. rextpg
71. ralpr
72. rexpr
73. reuprg0
74. reuprg
75. reurexprg
76. raltp
77. rextp
78. nfsn
79. csbsng
80. csbprg
81. elinsn
82. disjsn
83. disjsn2
84. disjpr2
85. disjprsn
86. disjtpsn
87. disjtp2
88. snprc
89. snnzb
90. rmosn
91. r19.12sn
92. rabsn
93. rabsnifsb
94. rabsnif
95. rabrsn
96. euabsn2
97. euabsn
98. reusn
99. absneu
100. rabsneu
101. eusn
102. rabsnt
103. prcom
104. preq1
105. preq2
106. preq12
107. preq1i
108. preq2i
109. preq12i
110. preq1d
111. preq2d
112. preq12d
113. tpeq1
114. tpeq2
115. tpeq3
116. tpeq1d
117. tpeq2d
118. tpeq3d
119. tpeq123d
120. tprot
121. tpcoma
122. tpcomb
123. tpass
124. qdass
125. qdassr
126. tpidm12
127. tpidm13
128. tpidm23
129. tpidm
130. tppreq3
131. prid1g
132. prid2g
133. prid1
134. prid2
135. ifpprsnss
136. prprc1
137. prprc2
138. prprc
139. tpid1
140. tpid1g
141. tpid2
142. tpid2g
143. tpid3g
144. tpid3
145. snnzg
146. snnz
147. prnz
148. prnzg
149. tpnz
150. tpnzd
151. raltpd
152. snssg
153. snss
154. eldifsn
155. ssdifsn
156. elpwdifsn
157. eldifsni
158. eldifsnneq
159. eldifsnneqOLD
160. neldifsn
161. neldifsnd
162. rexdifsn
163. raldifsni
164. raldifsnb
165. eldifvsn
166. difsn
167. difprsnss
168. difprsn1
169. difprsn2
170. diftpsn3
171. difpr
172. tpprceq3
173. tppreqb
174. difsnb
175. difsnpss
176. snssi
177. snssd
178. difsnid
179. eldifeldifsn
180. pw0
181. pwpw0
182. snsspr1
183. snsspr2
184. snsstp1
185. snsstp2
186. snsstp3
187. prssg
188. prss
189. prssi
190. prssd
191. prsspwg
192. ssprss
193. ssprsseq
194. sssn
195. ssunsn2
196. ssunsn
197. eqsn
198. issn
199. n0snor2el
200. ssunpr
201. sspr
202. sstp
203. tpss
204. tpssi
205. sneqrg
206. sneqr
207. snsssn
208. mosneq
209. sneqbg
210. snsspw
211. prsspw
212. preq1b
213. preq2b
214. preqr1
215. preqr2
216. preq12b
217. opthpr
218. preqr1g
219. preq12bg
220. prneimg
221. prnebg
222. pr1eqbg
223. pr1nebg
224. preqsnd
225. prnesn
226. prneprprc
227. preqsn
228. preq12nebg
229. prel12g
230. opthprneg
231. elpreqprlem
232. elpreqpr
233. elpreqprb
234. elpr2elpr
235. dfopif
236. dfopg
237. dfop
238. opeq1
239. opeq2
240. opeq12
241. opeq1i
242. opeq2i
243. opeq12i
244. opeq1d
245. opeq2d
246. opeq12d
247. oteq1
248. oteq2
249. oteq3
250. oteq1d
251. oteq2d
252. oteq3d
253. oteq123d
254. nfop
255. nfopd
256. csbopg
257. opidg
258. opid
259. ralunsn
260. 2ralunsn
261. opprc
262. opprc1
263. opprc2
264. oprcl
265. pwsn
266. pwsnOLD
267. pwpr
268. pwtp
269. pwpwpw0
270. pwv
271. prproe
272. 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. unipr
19. uniprg
20. unisng
21. unisn
22. unisn3
23. dfnfc2
24. uniun
25. uniin
26. ssuni
27. uni0b
28. uni0c
29. uni0
30. csbuni
31. elssuni
32. unissel
33. unissb
34. uniss2
35. unidif
36. ssunieq
37. unimax
38. 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. intpr
35. intprg
36. intsng
37. intsn
38. uniintsn
39. uniintab
40. intunsn
41. rint0
42. elrint
43. 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. 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. iunn0
72. iinab
73. iinrab
74. iinrab2
75. iunin2
76. iunin1
77. iinun2
78. iundif2
79. iindif1
80. 2iunin
81. iindif2
82. iinin2
83. iinin1
84. iinvdif
85. elriin
86. riin0
87. riinn0
88. riinrab
89. symdif0
90. symdifv
91. symdifid
92. iinxsng
93. iinxprg
94. iunxsng
95. iunxsn
96. iunxsngf
97. iunun
98. iunxun
99. iunxdif3
100. iunxprg
101. iunxiun
102. iinuni
103. iununi
104. sspwuni
105. pwssb
106. elpwpw
107. pwpwab
108. pwpwssunieq
109. elpwuni
110. iinpw
111. iunpwss
112. 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