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. clelsb1fw
26. clelsb1f
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
56. sbabelOLD
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. ralim
21. ralimi2
22. ralimia
23. ralimiaa
24. ralimi
25. 2ralimi
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. 2ralbiim
38. r19.21v
39. ralimdv2
40. ralimdva
41. ralimdv
42. ralimdvva
43. hbralrimi
44. ralrimiv
45. ralrimiva
46. ralrimivw
47. r19.27v
48. r19.28v
49. ralrimdv
50. ralrimdva
51. ralrimivv
52. ralrimivva
53. ralrimivvva
54. ralrimdvv
55. ralrimdvva
56. ralbidv2
57. ralbidva
58. ralbidv
59. 2ralbidva
60. 2ralbidv
61. r2allem
62. r2al
63. r3al
64. rgen2
65. rgen3
66. rspw
67. rsp
68. rspa
69. rspec
70. r19.21bi
71. r19.21be
72. rspec2
73. rspec3
74. rsp2
75. r19.21t
76. r19.21
77. ralrimi
78. ralimdaa
79. ralrimd
80. nfra1
81. hbra1
82. hbral
83. r2alf
84. nfraldw
85. nfraldwOLD
86. nfrald
87. nfralw
88. nfral
89. nfra2w
90. nfra2wOLD
91. nfra2wOLDOLD
92. nfra2
93. rgen2a
94. ralbida
95. ralbidaOLD
96. ralbid
97. 2ralbida
98. raleqbii
99. ralcom4
100. ralcom4OLD
101. ralnex
102. dfral2
103. rexnal
104. dfrex2
105. rexex
106. rexim
107. rexbi
108. rexbiOLD
109. reximi2
110. reximia
111. reximiaOLD
112. reximi
113. rexbii2
114. rexbiia
115. rexbii
116. 2rexbii
117. rexcom4
118. 2ex2rexrot
119. rexcom4a
120. rexanid
121. r19.29
122. r19.29r
123. r19.29imd
124. rexnal2
125. rexnal3
126. ralnex2
127. ralnex3
128. ralinexa
129. rexanali
130. nrexralim
131. risset
132. nelb
133. nelbOLD
134. nrex
135. nrexdv
136. reximdv2
137. reximdvai
138. reximdvaiOLD
139. reximdv
140. reximdva
141. reximddv
142. reximssdv
143. reximdvva
144. reximddv2
145. r19.23v
146. rexlimiv
147. rexlimiva
148. rexlimivw
149. rexlimdv
150. rexlimdva
151. rexlimdvaa
152. rexlimdv3a
153. rexlimdva2
154. r19.29an
155. r19.29a
156. rexlimdvw
157. rexlimddv
158. rexlimivv
159. rexlimdvv
160. rexlimdvva
161. rexbidv2
162. rexbidva
163. rexbidv
164. 2rexbiia
165. 2rexbidva
166. 2rexbidv
167. rexralbidv
168. r2exlem
169. r2ex
170. rspe
171. rsp2e
172. nfre1
173. nfrexd
174. nfrexdg
175. nfrex
176. nfrexg
177. reximdai
178. reximd2a
179. r19.23t
180. r19.23
181. rexlimi
182. rexlimd2
183. rexlimd
184. rexbida
185. rexbidvaALT
186. rexbid
187. rexbidvALT
188. ralrexbid
189. ralrexbidOLD
190. r19.12
191. r19.12OLD
192. r2exf
193. rexeqbii
194. reuanid
195. rmoanid
196. r19.29af2
197. r19.29af
198. 2r19.29
199. r19.29d2r
200. r19.29d2rOLD
201. r19.29vva
202. r19.29vvaOLD
203. r19.30
204. r19.30OLD
205. r19.32v
206. r19.35
207. r19.36v
208. r19.37
209. r19.37v
210. r19.40
211. r19.41v
212. r19.41
213. r19.41vv
214. r19.42v
215. r19.43
216. r19.44v
217. r19.45v
218. ralcom
219. rexcom
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. 2ralorOLD
234. nfreu1
235. nfrmo1
236. nfreud
237. nfrmod
238. nfrmow
239. nfreuw
240. nfreuwOLD
241. nfrmowOLD
242. nfreu
243. nfrmo
244. rabid
245. rabrab
246. rabidim1
247. rabid2f
248. rabid2
249. rabid2OLD
250. rabbi
251. nfrab1
252. nfrabw
253. nfrabwOLD
254. nfrab
255. reubida
256. reubidva
257. reubidv
258. reubiia
259. reubii
260. rmobida
261. rmobidva
262. rmobidvaOLD
263. rmobidv
264. rmobiia
265. rmobii
266. raleqf
267. rexeqf
268. reueq1f
269. rmoeq1f
270. raleqbidv
271. rexeqbidv
272. raleqbidvv
273. rexeqbidvv
274. raleqbi1dv
275. rexeqbi1dv
276. raleq
277. rexeq
278. reueq1
279. rmoeq1
280. raleqi
281. rexeqi
282. raleqdv
283. rexeqdv
284. reueqd
285. rmoeqd
286. raleqbid
287. rexeqbid
288. raleqbidva
289. rexeqbidva
290. raleleq
291. raleleqALT
292. moel
293. moelOLD
294. mormo
295. reu5
296. reurex
297. 2reu2rex
298. reurmo
299. rmo5
300. nrexrmo
301. reueubd
302. cbvralfw
303. cbvralfwOLD
304. cbvrexfw
305. cbvralf
306. cbvrexf
307. cbvralw
308. cbvrexw
309. cbvreuw
310. cbvrmow
311. cbvrmowOLD
312. cbvral
313. cbvrex
314. cbvreu
315. cbvrmo
316. cbvralvw
317. cbvrexvw
318. cbvrmovw
319. cbvreuvw
320. cbvreuvwOLD
321. cbvralv
322. cbvrexv
323. cbvreuv
324. cbvrmov
325. cbvraldva2
326. cbvrexdva2
327. cbvraldva
328. cbvrexdva
329. cbvral2vw
330. cbvrex2vw
331. cbvral3vw
332. cbvral2v
333. cbvrex2v
334. cbvral3v
335. cbvralsvw
336. cbvrexsvw
337. cbvralsv
338. cbvrexsv
339. sbralie
340. rabbiia
341. rabbii
342. rabbida
343. rabbid
344. rabbidva2
345. rabbia2
346. rabbidva
347. rabbidvaOLD
348. rabbidv
349. rabeqf
350. rabeqi
351. rabeqiOLD
352. rabeq
353. rabeqdv
354. rabeqbidv
355. rabeqbidva
356. rabeq2i
357. rabswap
358. cbvrabw
359. cbvrab
360. cbvrabv
361. rabrabi
362. rabrabiOLD
363. rabeqcda
364. ralrimia
365. 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. elex2OLD
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. ceqsexvOLD
50. ceqsexv2d
51. ceqsex2
52. ceqsex2v
53. ceqsex3v
54. ceqsex4v
55. ceqsex6v
56. ceqsex8v
57. gencbvex
58. gencbvex2
59. gencbval
60. sbhypf
61. vtoclgft
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. vtocl3g
81. vtoclgaf
82. vtoclga
83. vtocl2ga
84. vtocl2gaf
85. vtocl3gaf
86. vtocl3ga
87. vtocl3gaOLD
88. vtocl4g
89. vtocl4ga
90. vtocleg
91. vtoclegft
92. vtoclef
93. vtocle
94. vtoclri
95. spcimgft
96. spcgft
97. spcimgf
98. spcimegf
99. spcgf
100. spcegf
101. spcimdv
102. spcdv
103. spcimedv
104. spcgv
105. spcegv
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. rspcdv2
126. rspcv
127. rspcvOLD
128. rspccv
129. rspcva
130. rspccva
131. rspcev
132. rspcevOLD
133. rspcdva
134. rspcedvd
135. rspcime
136. rspceaimv
137. rspcedeq1vd
138. rspcedeq2vd
139. rspc2
140. rspc2gv
141. rspc2v
142. rspc2va
143. rspc2ev
144. rspc3v
145. rspc3ev
146. rspceeqv
147. ralxpxfr2d
148. rexraleqim
149. eqvincg
150. eqvinc
151. eqvincf
152. alexeqg
153. ceqex
154. ceqsexg
155. ceqsexgv
156. ceqsexgvOLD
157. ceqsrexv
158. ceqsrexbv
159. ceqsrex2v
160. clel2g
161. clel2gOLD
162. clel2
163. clel3g
164. clel3
165. clel4g
166. clel4
167. clel4OLD
168. clel5
169. pm13.183
170. rr19.3v
171. rr19.28v
172. elab6g
173. elabd2
174. elabd3
175. elabgt
176. elabgtOLD
177. elabgf
178. elabf
179. elabg
180. elabgOLD
181. elab
182. elabOLD
183. elab2g
184. elabd
185. elab2
186. elab4g
187. elab3gf
188. elab3g
189. elab3
190. elrabi
191. elrabiOLD
192. elrabf
193. rabtru
194. rabeqc
195. elrab3t
196. elrab
197. elrab3
198. elrabd
199. elrab2
200. ralab
201. ralabOLD
202. ralrab
203. rexab
204. rexabOLD
205. rexrab
206. ralab2
207. ralab2OLD
208. ralrab2
209. rexab2
210. rexab2OLD
211. rexrab2
212. abidnf
213. dedhb
214. nelrdva
215. eqeu
216. moeq
217. eueq
218. eueqi
219. eueq2
220. eueq3
221. moeq3
222. mosub
223. mo2icl
224. mob2
225. moi2
226. mob
227. moi
228. morex
229. euxfr2w
230. euxfrw
231. euxfr2
232. euxfr
233. euind
234. reu2
235. reu6
236. reu3
237. reu6i
238. eqreu
239. rmo4
240. reu4
241. reu7
242. reu8
243. rmo3f
244. rmo4f
245. reu2eqd
246. reueq
247. rmoeq
248. rmoan
249. rmoim
250. rmoimia
251. rmoimi
252. rmoimi2
253. 2reu5a
254. reuimrmo
255. 2reuswap
256. 2reuswap2
257. reuxfrd
258. reuxfr
259. reuxfr1d
260. reuxfr1ds
261. reuxfr1
262. reuind
263. 2rmorex
264. 2reu5lem1
265. 2reu5lem2
266. 2reu5lem3
267. 2reu5
268. 2reurmo
269. 2reurex
270. 2rmoswap
271. 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. sbc5ALT
31. sbc6g
32. sbc6gOLD
33. sbc6
34. sbc7
35. cbvsbcw
36. cbvsbcvw
37. cbvsbc
38. cbvsbcv
39. sbciegft
40. sbciegf
41. sbcieg
42. sbciegOLD
43. sbcie2g
44. sbcie
45. sbciedf
46. sbcied
47. sbciedOLD
48. sbcied2
49. elrabsf
50. eqsbc1
51. sbcng
52. sbcimg
53. sbcan
54. sbcor
55. sbcbig
56. sbcn1
57. sbcim1
58. sbcim1OLD
59. sbcbid
60. sbcbidv
61. sbcbidvOLD
62. sbcbii
63. sbcbi1
64. sbcbi2
65. sbcbi2OLD
66. sbcal
67. sbcex2
68. sbceqal
69. sbceqalOLD
70. sbeqalb
71. eqsbc2
72. sbc3an
73. sbcel1v
74. sbcel2gv
75. sbcel21v
76. sbcimdv
77. sbcimdvOLD
78. sbctt
79. sbcgf
80. sbc19.21g
81. sbcg
82. sbcgOLD
83. sbcgfi
84. sbc2iegf
85. sbc2ie
86. sbc2ieOLD
87. sbc2iedv
88. sbc3ie
89. sbccomlem
90. sbccom
91. sbcralt
92. sbcrext
93. sbcralg
94. sbcrex
95. sbcreu
96. reu8nf
97. sbcabel
98. rspsbc
99. rspsbca
100. rspesbca
101. spesbc
102. spesbcd
103. sbcth2
104. ra4v
105. ra4
106. rmo2
107. rmo2i
108. rmo3
109. rmob
110. rmoi
111. rmob2
112. rmoi2
113. rmoanim
114. rmoanimALT
115. reuan
116. 2reu1
117. 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. csbconstgOLD
22. csbgfi
23. csbconstgi
24. nfcsb1d
25. nfcsb1
26. nfcsb1v
27. nfcsbd
28. nfcsbw
29. nfcsb
30. csbhypf
31. csbiebt
32. csbiedf
33. csbieb
34. csbiebg
35. csbiegf
36. csbief
37. csbie
38. csbieOLD
39. csbied
40. csbiedOLD
41. csbied2
42. csbie2t
43. csbie2
44. csbie2g
45. cbvrabcsfw
46. cbvralcsf
47. cbvrexcsf
48. cbvreucsf
49. cbvrabcsf
50. cbvralv2
51. cbvrexv2
52. 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. sselid
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. ab0w
53. ab0
54. ab0OLD
55. ab0ALT
56. dfnf5
57. ab0orv
58. ab0orvALT
59. abn0
60. abn0OLD
61. rab0
62. rabeq0w
63. rabeq0
64. rabn0
65. rabxm
66. rabnc
67. elneldisj
68. elnelun
69. un0
70. in0
71. 0un
72. 0in
73. inv1
74. unv
75. 0ss
76. ss0b
77. ss0
78. sseq0
79. ssn0
80. 0dif
81. abf
82. abfOLD
83. eq0rdv
84. eq0rdvALT
85. csbprc
86. csb0
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
203. csbdif
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. opeq2
247. opeq12
248. opeq1i
249. opeq2i
250. opeq12i
251. opeq1d
252. opeq2d
253. opeq12d
254. oteq1
255. oteq2
256. oteq3
257. oteq1d
258. oteq2d
259. oteq3d
260. oteq123d
261. nfop
262. nfopd
263. csbopg
264. opidg
265. opid
266. ralunsn
267. 2ralunsn
268. opprc
269. opprc1
270. opprc2
271. oprcl
272. pwsn
273. pwsnOLD
274. pwpr
275. pwtp
276. pwpwpw0
277. pwv
278. prproe
279. 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. nfopabd
8. nfopab
9. nfopab1
10. nfopab2
11. cbvopab
12. cbvopabv
13. cbvopabvOLD
14. cbvopab1
15. cbvopab1g
16. cbvopab2
17. cbvopab1s
18. cbvopab1v
19. cbvopab1vOLD
20. cbvopab2v
21. unopab
Functions in maps-to notation
1. cmpt
2. df-mpt
3. mpteq12da
4. mpteq12df
5. mpteq12dfOLD
6. mpteq12f
7. mpteq12dva
8. mpteq12dvaOLD
9. mpteq12dv
10. mpteq12
11. mpteq1
12. mpteq1OLD
13. mpteq1d
14. mpteq1i
15. mpteq1iOLD
16. mpteq2da
17. mpteq2daOLD
18. mpteq2dva
19. mpteq2dvaOLD
20. mpteq2dv
21. mpteq2ia
22. mpteq2iaOLD
23. mpteq2i
24. mpteq12i
25. nfmpt
26. nfmpt1
27. cbvmptf
28. cbvmptfg
29. cbvmpt
30. cbvmptg
31. cbvmptv
32. cbvmptvOLD
33. cbvmptvg
34. 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