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. nfceqi
18. nfcxfr
19. nfcxfrd
20. nfcv
21. nfcvd
22. nfab1
23. nfnfc1
24. clelsb3fw
25. clelsb3f
26. nfab
27. nfabg
28. nfaba1
29. nfaba1g
30. nfeqd
31. nfeld
32. nfnfc
33. nfeq
34. nfel
35. nfeq1
36. nfel1
37. nfeq2
38. nfel2
39. drnfc1
40. drnfc2
41. nfabdw
42. nfabd
43. nfabd2
44. dvelimdc
45. dvelimc
46. nfcvf
47. nfcvf2
48. cleqf
49. abid2f
50. abeq2f
51. 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. reximia
101. reximi
102. reximi2
103. rexbii2
104. rexbiia
105. rexbii
106. 2rexbii
107. rexcom4
108. 2ex2rexrot
109. rexcom4a
110. rexanid
111. r19.29
112. r19.29r
113. r19.29imd
114. rexnal2
115. rexnal3
116. ralnex2
117. ralnex3
118. ralinexa
119. rexanali
120. nrexralim
121. risset
122. nelb
123. nrex
124. nrexdv
125. reximdv2
126. reximdvai
127. reximdv
128. reximdva
129. reximddv
130. reximssdv
131. reximdvva
132. reximddv2
133. r19.23v
134. rexlimiv
135. rexlimiva
136. rexlimivw
137. rexlimdv
138. rexlimdva
139. rexlimdvaa
140. rexlimdv3a
141. rexlimdva2
142. r19.29an
143. r19.29a
144. rexlimdvw
145. rexlimddv
146. rexlimivv
147. rexlimdvv
148. rexlimdvva
149. rexbidv2
150. rexbidva
151. rexbidv
152. 2rexbiia
153. 2rexbidva
154. 2rexbidv
155. rexralbidv
156. r2exlem
157. r2ex
158. rspe
159. rsp2e
160. nfre1
161. nfrexd
162. nfrexdg
163. nfrex
164. nfrexg
165. reximdai
166. reximd2a
167. r19.23t
168. r19.23
169. rexlimi
170. rexlimd2
171. rexlimd
172. rexbida
173. rexbidvaALT
174. rexbid
175. rexbidvALT
176. ralrexbid
177. ralrexbidOLD
178. r19.12
179. r2exf
180. rexeqbii
181. reuanid
182. rmoanid
183. r19.29af2
184. r19.29af
185. 2r19.29
186. r19.29d2r
187. r19.29vva
188. r19.30
189. r19.32v
190. r19.35
191. r19.36v
192. r19.37
193. r19.37v
194. r19.40
195. r19.41v
196. r19.41
197. r19.41vv
198. r19.42v
199. r19.43
200. r19.44v
201. r19.45v
202. ralcom
203. rexcom
204. rexcomOLD
205. ralcomf
206. rexcomf
207. ralcom13
208. rexcom13
209. ralrot3
210. rexrot4
211. ralcom2
212. ralcom3
213. reeanlem
214. reean
215. reeanv
216. 3reeanv
217. 2ralor
218. nfreu1
219. nfrmo1
220. nfreud
221. nfrmod
222. nfreuw
223. nfrmow
224. nfreu
225. nfrmo
226. rabid
227. rabrab
228. rabidim1
229. rabid2
230. rabid2f
231. rabbi
232. nfrab1
233. nfrabw
234. nfrab
235. reubida
236. reubidva
237. reubidv
238. reubiia
239. reubii
240. rmobida
241. rmobidva
242. rmobidv
243. rmobiia
244. rmobii
245. raleqf
246. rexeqf
247. reueq1f
248. rmoeq1f
249. raleqbidv
250. rexeqbidv
251. raleqbi1dv
252. rexeqbi1dv
253. raleq
254. rexeq
255. reueq1
256. rmoeq1
257. raleqi
258. rexeqi
259. raleqdv
260. rexeqdv
261. reueqd
262. rmoeqd
263. raleqbid
264. rexeqbid
265. raleqbidva
266. rexeqbidva
267. raleleq
268. raleleqALT
269. mormo
270. reu5
271. reurex
272. 2reu2rex
273. reurmo
274. rmo5
275. nrexrmo
276. reueubd
277. cbvralfw
278. cbvralfwOLD
279. cbvrexfw
280. cbvralf
281. cbvrexf
282. cbvralw
283. cbvrexw
284. cbvreuw
285. cbvrmow
286. cbvrmowOLD
287. cbvral
288. cbvrex
289. cbvreu
290. cbvrmo
291. cbvralvw
292. cbvrexvw
293. cbvreuvw
294. cbvralv
295. cbvrexv
296. cbvreuv
297. cbvrmov
298. cbvraldva2
299. cbvrexdva2
300. cbvrexdva2OLD
301. cbvraldva
302. cbvrexdva
303. cbvral2vw
304. cbvrex2vw
305. cbvral3vw
306. cbvral2v
307. cbvrex2v
308. cbvral3v
309. cbvralsvw
310. cbvrexsvw
311. cbvralsv
312. cbvrexsv
313. sbralie
314. rabbiia
315. rabbii
316. rabbida
317. rabbid
318. rabbidva2
319. rabbia2
320. rabbidva
321. rabbidvaOLD
322. rabbidv
323. rabeqf
324. rabeqi
325. rabeqiOLD
326. rabeq
327. rabeqdv
328. rabeqbidv
329. rabeqbidva
330. rabeq2i
331. rabswap
332. cbvrabw
333. cbvrab
334. cbvrabv
335. 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. cgsex4gOLD
48. ceqsex
49. ceqsexv
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. vtoclgftOLD
63. vtocldf
64. vtocld
65. vtocl2d
66. vtoclf
67. vtocl
68. vtoclALT
69. vtocl2
70. vtocl2OLD
71. vtocl3
72. vtoclb
73. vtoclgf
74. vtoclg1f
75. vtoclg
76. vtoclgOLD
77. vtoclbg
78. vtocl2gf
79. vtocl3gf
80. vtocl2g
81. vtoclgaf
82. vtoclga
83. vtocl2ga
84. vtocl2gaf
85. vtocl3gaf
86. vtocl3ga
87. vtocl4g
88. vtocl4ga
89. vtocleg
90. vtoclegft
91. vtoclef
92. vtocle
93. vtoclri
94. spcimgft
95. spcgft
96. spcimgf
97. spcimegf
98. spcgf
99. spcegf
100. spcimdv
101. spcdv
102. spcimedv
103. spcgv
104. spcgvOLD
105. spcegv
106. spcegvOLD
107. spcedv
108. spc2egv
109. spc2gv
110. spc2ed
111. spc2d
112. spc3egv
113. spc3gv
114. spcv
115. spcev
116. spc2ev
117. rspct
118. rspcdf
119. rspc
120. rspce
121. rspcimdv
122. rspcimedv
123. rspcdv
124. rspcedv
125. rspcebdv
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. clel2
162. clel3g
163. clel3
164. clel4
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. elrabf
185. rabtru
186. rabeqc
187. elrab3t
188. elrab
189. elrab3
190. elrabd
191. elrab2
192. ralab
193. ralrab
194. rexab
195. rexrab
196. ralab2
197. ralab2OLD
198. ralrab2
199. rexab2
200. rexab2OLD
201. rexrab2
202. abidnf
203. dedhb
204. nelrdva
205. eqeu
206. moeq
207. eueq
208. eueqi
209. eueq2
210. eueq3
211. moeq3
212. mosub
213. mo2icl
214. mob2
215. moi2
216. mob
217. moi
218. morex
219. euxfr2w
220. euxfrw
221. euxfr2
222. euxfr
223. euind
224. reu2
225. reu6
226. reu3
227. reu6i
228. eqreu
229. rmo4
230. reu4
231. reu7
232. reu8
233. rmo3f
234. rmo4f
235. reu2eqd
236. reueq
237. rmoeq
238. rmoan
239. rmoim
240. rmoimia
241. rmoimi
242. rmoimi2
243. 2reu5a
244. reuimrmo
245. 2reuswap
246. 2reuswap2
247. reuxfrd
248. reuxfr
249. reuxfr1d
250. reuxfr1ds
251. reuxfr1
252. reuind
253. 2rmorex
254. 2reu5lem1
255. 2reu5lem2
256. 2reu5lem3
257. 2reu5
258. 2reurex
259. 2reurmo
260. 2rmoswap
261. 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
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. ssrab3
112. rabssrabd
113. ssrabeq
114. rabssab
115. uniiunlem
116. dfpss2
117. dfpss3
118. psseq1
119. psseq2
120. psseq1i
121. psseq2i
122. psseq12i
123. psseq1d
124. psseq2d
125. psseq12d
126. pssss
127. pssne
128. pssssd
129. pssned
130. sspss
131. pssirr
132. pssn2lp
133. sspsstri
134. ssnpss
135. psstr
136. sspsstr
137. psssstr
138. psstrd
139. sspsstrd
140. psssstrd
141. npss
142. ssnelpss
143. ssnelpssd
144. 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. noel
6. nel02
7. n0i
8. ne0i
9. ne0d
10. n0ii
11. ne0ii
12. vn0
13. eq0f
14. neq0f
15. n0f
16. eq0
17. neq0
18. n0
19. eq0OLD
20. neq0OLD
21. n0OLD
22. nel0
23. reximdva0
24. rspn0
25. rspn0OLD
26. n0rex
27. ssn0rex
28. n0moeu
29. rex0
30. reu0
31. rmo0
32. 0el
33. n0el
34. eqeuel
35. ssdif0
36. difn0
37. pssdifn0
38. pssdif
39. ndisj
40. difin0ss
41. inssdif0
42. difid
43. difidALT
44. dif0
45. ab0
46. dfnf5
47. ab0orv
48. abn0
49. rab0
50. rabeq0
51. rabn0
52. rabxm
53. rabnc
54. elneldisj
55. elnelun
56. un0
57. in0
58. 0un
59. 0in
60. inv1
61. unv
62. 0ss
63. ss0b
64. ss0
65. sseq0
66. ssn0
67. 0dif
68. abf
69. abfOLD
70. eq0rdv
71. csbprc
72. csb0
73. csb0OLD
74. sbcel12
75. sbceqg
76. sbceqi
77. sbcnel12g
78. sbcne12
79. sbcel1g
80. sbceq1g
81. sbcel2
82. sbceq2g
83. csbcom
84. sbcnestgfw
85. csbnestgfw
86. sbcnestgw
87. csbnestgw
88. sbcco3gw
89. sbcnestgf
90. csbnestgf
91. sbcnestg
92. csbnestg
93. sbcco3g
94. csbco3g
95. csbnest1g
96. csbidm
97. csbvarg
98. csbvargi
99. sbccsb
100. sbccsb2
101. rspcsbela
102. sbnfc2
103. csbab
104. csbun
105. csbin
106. csbie2df
107. 2nreu
108. un00
109. vss
110. 0pss
111. npss0
112. pssv
113. disj
114. disjOLD
115. disjr
116. disj1
117. reldisj
118. reldisjOLD
119. disj3
120. disjne
121. disjeq0
122. disjel
123. disj2
124. disj4
125. ssdisj
126. disjpss
127. undisj1
128. undisj2
129. ssindif0
130. inelcm
131. minel
132. undif4
133. disjssun
134. vdif0
135. difrab0eq
136. pssnel
137. disjdif
138. difin0
139. unvdif
140. undif1
141. undif2
142. undifabs
143. inundif
144. disjdif2
145. difun2
146. undif
147. ssdifin0
148. ssdifeq0
149. ssundif
150. difcom
151. pssdifcom1
152. pssdifcom2
153. difdifdir
154. uneqdifeq
155. raldifeq
156. r19.2z
157. r19.2zb
158. r19.3rz
159. r19.28z
160. r19.3rzv
161. r19.9rzv
162. r19.28zv
163. r19.37zv
164. r19.45zv
165. r19.44zv
166. r19.27z
167. r19.27zv
168. r19.36zv
169. rzal
170. rexn0
171. ralidm
172. ral0
173. ralf0
174. ralnralall
175. falseral0
176. raaan
177. raaanv
178. sbss
179. sbcssg
180. raaan2
181. 2reu4lem
182. 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. 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. dfopg
239. dfop
240. opeq1
241. opeq1OLD
242. opeq2
243. opeq2OLD
244. opeq12
245. opeq1i
246. opeq2i
247. opeq12i
248. opeq1d
249. opeq2d
250. opeq12d
251. oteq1
252. oteq2
253. oteq3
254. oteq1d
255. oteq2d
256. oteq3d
257. oteq123d
258. nfop
259. nfopd
260. csbopg
261. opidg
262. opid
263. ralunsn
264. 2ralunsn
265. opprc
266. opprc1
267. opprc2
268. oprcl
269. pwsn
270. pwsnOLD
271. pwpr
272. pwtp
273. pwpwpw0
274. pwv
275. prproe
276. 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. 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