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. nfcrii
12. nfceqdf
13. nfceqi
14. nfcxfr
15. nfcxfrd
16. nfcv
17. nfcvd
18. nfab1
19. nfnfc1
20. clelsb1fw
21. clelsb1f
22. nfab
23. nfabg
24. nfaba1
25. nfaba1OLD
26. nfaba1g
27. nfeqd
28. nfeld
29. nfnfc
30. nfeq
31. nfel
32. nfeq1
33. nfel1
34. nfeq2
35. nfel2
36. drnfc1
37. drnfc2
38. nfabdw
39. nfabd
40. nfabd2
41. dvelimdc
42. dvelimc
43. nfcvf
44. nfcvf2
45. cleqf
46. eqabf
47. abid2f
48. abid2fOLD
49. sbabel
Negated equality and membership
1. Negated equality
2. Negated membership
Restricted quantification
1. Restricted universal and existential quantification
2. Restricted existential uniqueness and at-most-one quantifier
3. Restricted class abstraction
The universal class
1. cvv
2. vjust
3. df-v
4. dfv2
5. vex
6. elv
7. elvd
8. el2v
9. el3v
10. el3v3
11. eqv
12. eqvf
13. abv
14. abvALT
15. isset
16. cbvexeqsetf
17. issetft
18. issetf
19. isseti
20. issetri
21. eqvisset
22. elex
23. elexOLD
24. elexi
25. elexd
26. elex2OLD
27. elex22
28. prcnel
29. ralv
30. rexv
31. reuv
32. rmov
33. rabab
34. rexcom4b
35. ceqsal1t
36. ceqsalt
37. ceqsralt
38. ceqsalg
39. ceqsalgALT
40. ceqsal
41. ceqsalALT
42. ceqsalv
43. ceqsralv
44. gencl
45. 2gencl
46. 3gencl
47. cgsexg
48. cgsex2g
49. cgsex4g
50. cgsex4gOLD
51. ceqsex
52. ceqsexOLD
53. ceqsexv
54. ceqsexv2d
55. ceqsexv2dOLD
56. ceqsex2
57. ceqsex2v
58. ceqsex3v
59. ceqsex4v
60. ceqsex6v
61. ceqsex8v
62. gencbvex
63. gencbvex2
64. gencbval
65. sbhypf
66. sbhypfOLD
67. spcimgft
68. spcimgfi1
69. spcimgfi1OLD
70. spcgft
71. spcimgf
72. spcimegf
73. vtoclgft
74. vtocleg
75. vtoclg
76. vtocle
77. vtocleOLD
78. vtoclbg
79. vtocl
80. vtoclOLD
81. vtocldf
82. vtocld
83. vtocl2d
84. vtoclef
85. vtoclf
86. vtoclfOLD
87. vtocl2
88. vtocl3
89. vtoclb
90. vtoclgf
91. vtoclg1f
92. vtoclgOLD
93. vtocl2gf
94. vtocl3gf
95. vtocl2g
96. vtocl3g
97. vtoclgaf
98. vtoclga
99. vtocl2ga
100. vtocl2gaf
101. vtocl2gafOLD
102. vtocl3gaf
103. vtocl3gafOLD
104. vtocl3ga
105. vtocl3gaOLD
106. vtocl4g
107. vtocl4ga
108. vtocl4gaOLD
109. vtoclegft
110. vtoclegftOLD
111. vtoclri
112. spcgf
113. spcegf
114. spcimdv
115. spcdv
116. spcimedv
117. spcgv
118. spcegv
119. spcedv
120. spc2egv
121. spc2gv
122. spc2ed
123. spc2d
124. spc3egv
125. spc3gv
126. spcv
127. spcev
128. spc2ev
129. rspct
130. rspcdf
131. rspc
132. rspce
133. rspcimdv
134. rspcimedv
135. rspcdv
136. rspcedv
137. rspcebdv
138. rspcdv2
139. rspcv
140. rspccv
141. rspcva
142. rspccva
143. rspcev
144. rspcdva
145. rspcedvd
146. rspcedvdw
147. rspceb2dv
148. rspcime
149. rspceaimv
150. rspcedeq1vd
151. rspcedeq2vd
152. rspc2
153. rspc2gv
154. rspc2v
155. rspc2va
156. rspc2ev
157. 2rspcedvdw
158. rspc2dv
159. rspc3v
160. rspc3ev
161. 3rspcedvdw
162. rspc3dv
163. rspc4v
164. rspc6v
165. rspc8v
166. rspceeqv
167. ralxpxfr2d
168. rexraleqim
169. eqvincg
170. eqvinc
171. eqvincf
172. alexeqg
173. ceqex
174. ceqsexg
175. ceqsexgv
176. ceqsrexv
177. ceqsrexbv
178. ceqsralbv
179. ceqsrex2v
180. clel2g
181. clel2
182. clel3g
183. clel3
184. clel4g
185. clel4
186. clel5
187. pm13.183
188. rr19.3v
189. rr19.28v
190. elab6g
191. elabd2
192. elabd3
193. elabgt
194. elabgtOLD
195. elabgf
196. elabf
197. elabg
198. elabgw
199. elab2gw
200. elab
201. elab2g
202. elabd
203. elab2
204. elab4g
205. elab3gf
206. elab3g
207. elab3
208. elrabi
209. elrabf
210. rabtru
211. rabeqcOLD
212. elrab3t
213. elrab
214. elrab3
215. elrabd
216. elrab2
217. elrab2w
218. ralab
219. ralrab
220. rexab
221. rexrab
222. ralab2
223. ralrab2
224. rexab2
225. rexrab2
226. reurab
227. abidnf
228. dedhb
229. class2seteq
230. nelrdva
231. eqeu
232. moeq
233. eueq
234. eueqi
235. eueq2
236. eueq3
237. moeq3
238. mosub
239. mo2icl
240. mob2
241. moi2
242. mob
243. moi
244. morex
245. euxfr2w
246. euxfrw
247. euxfr2
248. euxfr
249. euind
250. reu2
251. reu6
252. reu3
253. reu6i
254. eqreu
255. rmo4
256. reu4
257. reu7
258. reu8
259. rmo3f
260. rmo4f
261. reu2eqd
262. reueq
263. rmoeq
264. rmoan
265. rmoim
266. rmoimia
267. rmoimi
268. rmoimi2
269. 2reu5a
270. reuimrmo
271. 2reuswap
272. 2reuswap2
273. reuxfrd
274. reuxfr
275. reuxfr1d
276. reuxfr1ds
277. reuxfr1
278. reuind
279. 2rmorex
280. 2reu5lem1
281. 2reu5lem2
282. 2reu5lem3
283. 2reu5
284. 2reurmo
285. 2reurex
286. 2rmoswap
287. 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
3. ruOLD
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. sbciegftOLD
40. sbciegf
41. sbcieg
42. sbcie2g
43. sbcie
44. sbciedf
45. sbcied
46. sbcied2
47. elrabsf
48. eqsbc1
49. sbcng
50. sbcimg
51. sbcan
52. sbcor
53. sbcbig
54. sbcn1
55. sbcim1
56. sbcbid
57. sbcbidv
58. sbcbii
59. sbcbi1
60. sbcbi2
61. sbcal
62. sbcex2
63. sbceqal
64. sbeqalb
65. eqsbc2
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. sbccomlemOLD
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. 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. dfss2
3. dfss
4. df-pss
5. dfss3
6. dfss6
7. dfssf
8. dfss3f
9. nfss
10. ssel
11. ssel2
12. sseli
13. sselii
14. sselid
15. sseld
16. sselda
17. sseldd
18. ssneld
19. ssneldd
20. ssriv
21. ssrd
22. ssrdv
23. sstr2
24. sstr2OLD
25. sstr
26. sstri
27. sstrd
28. sstrid
29. sstrdi
30. sylan9ss
31. sylan9ssr
32. eqss
33. eqssi
34. eqssd
35. sssseq
36. eqrd
37. eqri
38. eqelssd
39. ssid
40. ssidd
41. ssv
42. sseq1
43. sseq2
44. sseq12
45. sseq1i
46. sseq2i
47. sseq12i
48. sseq1d
49. sseq2d
50. sseq12d
51. eqsstrd
52. eqsstrrd
53. sseqtrd
54. sseqtrrd
55. eqsstrid
56. eqsstrrid
57. sseqtrdi
58. sseqtrrdi
59. sseqtrid
60. sseqtrrid
61. eqsstrdi
62. eqsstrrdi
63. eqsstri
64. eqsstrri
65. sseqtri
66. sseqtrri
67. 3sstr3i
68. 3sstr4i
69. 3sstr3g
70. 3sstr4g
71. 3sstr3d
72. 3sstr4d
73. eqimssd
74. eqimsscd
75. eqimss
76. eqimss2
77. eqimssi
78. eqimss2i
79. nssne1
80. nssne2
81. nss
82. nelss
83. ssrexf
84. ssrmof
85. ssralv
86. ssrexv
87. ss2ralv
88. ss2rexv
89. ssralvOLD
90. ssrexvOLD
91. ralss
92. rexss
93. ralssOLD
94. rexssOLD
95. ss2ab
96. abss
97. ssab
98. ssabral
99. ss2abdv
100. ss2abi
101. abssdv
102. abssdvOLD
103. abssi
104. ss2rab
105. rabss
106. ssrab
107. ssrabdv
108. rabssdv
109. ss2rabdv
110. ss2rabi
111. rabss2
112. ssab2
113. ssrab2
114. rabss3d
115. ssrab3
116. rabssrabd
117. ssrabeq
118. rabssab
119. eqrrabd
120. uniiunlem
121. dfpss2
122. dfpss3
123. psseq1
124. psseq2
125. psseq1i
126. psseq2i
127. psseq12i
128. psseq1d
129. psseq2d
130. psseq12d
131. pssss
132. pssne
133. pssssd
134. pssned
135. sspss
136. pssirr
137. pssn2lp
138. sspsstri
139. ssnpss
140. psstr
141. sspsstr
142. psssstr
143. psstrd
144. sspsstrd
145. psssstrd
146. npss
147. ssnelpss
148. ssnelpssd
149. 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. 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. nel0
23. reximdva0
24. rspn0
25. n0rex
26. ssn0rex
27. n0moeu
28. rex0
29. reu0
30. rmo0
31. 0el
32. n0el
33. eqeuel
34. ssdif0
35. difn0
36. pssdifn0
37. pssdif
38. ndisj
39. inn0f
40. inn0
41. difin0ss
42. inssdif0
43. inindif
44. difid
45. difidALT
46. dif0
47. ab0w
48. ab0
49. ab0ALT
50. dfnf5
51. ab0orv
52. ab0orvALT
53. abn0
54. rab0
55. rabeq0w
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. eq0rdv
76. eq0rdvALT
77. csbprc
78. csb0
79. sbcel12
80. sbceqg
81. sbceqi
82. sbcnel12g
83. sbcne12
84. sbcel1g
85. sbceq1g
86. sbcel2
87. sbceq2g
88. csbcom
89. sbcnestgfw
90. csbnestgfw
91. sbcnestgw
92. csbnestgw
93. sbcco3gw
94. sbcnestgf
95. csbnestgf
96. sbcnestg
97. csbnestg
98. sbcco3g
99. csbco3g
100. csbnest1g
101. csbidm
102. csbvarg
103. csbvargi
104. sbccsb
105. sbccsb2
106. rspcsbela
107. sbnfc2
108. csbab
109. csbun
110. csbin
111. csbie2df
112. 2nreu
113. un00
114. vss
115. 0pss
116. npss0
117. pssv
118. disj
119. disjr
120. disj1
121. reldisj
122. disj3
123. disjne
124. disjeq0
125. disjel
126. disj2
127. disj4
128. ssdisj
129. disjpss
130. undisj1
131. undisj2
132. ssindif0
133. inelcm
134. minel
135. undif4
136. disjssun
137. vdif0
138. difrab0eq
139. pssnel
140. disjdif
141. disjdifr
142. difin0
143. unvdif
144. undif1
145. undif2
146. undifabs
147. inundif
148. disjdif2
149. difun2
150. undif
151. undifr
152. undifrOLD
153. undif5
154. ssdifin0
155. ssdifeq0
156. ssundif
157. difcom
158. pssdifcom1
159. pssdifcom2
160. difdifdir
161. uneqdifeq
162. raldifeq
163. r19.2z
164. r19.2zb
165. r19.3rz
166. r19.28z
167. r19.3rzv
168. r19.9rzv
169. r19.28zv
170. r19.37zv
171. r19.45zv
172. r19.44zv
173. r19.27z
174. r19.27zv
175. r19.36zv
176. ralidmw
177. rzal
178. rzalALT
179. rexn0
180. ralidm
181. ral0
182. ralf0
183. ralnralall
184. falseral0
185. raaan
186. raaanv
187. sbss
188. sbcssg
189. raaan2
190. 2reu4lem
191. 2reu4
192. 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. iftrueb
15. ifsb
16. dfif3
17. dfif4
18. dfif5
19. ifssun
20. ifeq12
21. ifeq1d
22. ifeq2d
23. ifeq12d
24. ifbi
25. ifbid
26. ifbieq1d
27. ifbieq2i
28. ifbieq2d
29. ifbieq12i
30. ifbieq12d
31. nfifd
32. nfif
33. ifeq1da
34. ifeq2da
35. ifeq12da
36. ifbieq12d2
37. ifclda
38. ifeqda
39. elimif
40. ifbothda
41. ifboth
42. ifid
43. eqif
44. ifval
45. elif
46. ifel
47. ifcl
48. ifcld
49. ifcli
50. ifexd
51. ifexg
52. ifex
53. ifeqor
54. ifnot
55. ifan
56. ifor
57. 2if2
58. ifcomnan
59. 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. elpwd
8. elpwi
9. elpwb
10. elpwid
11. elelpwi
12. sspw
13. sspwi
14. sspwd
15. pweq
16. pweqALT
17. pweqi
18. pweqd
19. pwunss
20. nfpw
21. pwidg
22. pwidb
23. pwid
24. pwss
25. 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. rabsneq
21. absn
22. dfpr2
23. dfsn2ALT
24. elprg
25. elpri
26. elpr
27. elpr2g
28. elpr2
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. rabeqsnd
46. ralsnsg
47. rexsns
48. rexsngf
49. ralsngf
50. reusngf
51. ralsng
52. rexsng
53. reusng
54. 2ralsng
55. rexreusng
56. exsnrex
57. ralsn
58. rexsn
59. elunsn
60. elpwunsn
61. eqoreldif
62. eltpg
63. eldiftp
64. eltpi
65. eltp
66. el7g
67. dftp2
68. nfpr
69. ifpr
70. ralprgf
71. rexprgf
72. ralprg
73. rexprg
74. raltpg
75. rextpg
76. ralpr
77. rexpr
78. reuprg0
79. reuprg
80. reurexprg
81. raltp
82. rextp
83. nfsn
84. csbsng
85. csbprg
86. elinsn
87. disjsn
88. disjsn2
89. disjpr2
90. disjprsn
91. disjtpsn
92. disjtp2
93. snprc
94. snnzb
95. rmosn
96. r19.12sn
97. rabsn
98. rabsnifsb
99. rabsnif
100. rabrsn
101. euabsn2
102. euabsn
103. reusn
104. absneu
105. rabsneu
106. eusn
107. rabsnt
108. prcom
109. preq1
110. preq2
111. preq12
112. preq1i
113. preq2i
114. preq12i
115. preq1d
116. preq2d
117. preq12d
118. tpeq1
119. tpeq2
120. tpeq3
121. tpeq1d
122. tpeq2d
123. tpeq3d
124. tpeq123d
125. tprot
126. tpcoma
127. tpcomb
128. tpass
129. qdass
130. qdassr
131. tpidm12
132. tpidm13
133. tpidm23
134. tpidm
135. tppreq3
136. prid1g
137. prid2g
138. prid1
139. prid2
140. ifpprsnss
141. prprc1
142. prprc2
143. prprc
144. tpid1
145. tpid1g
146. tpid2
147. tpid2g
148. tpid3g
149. tpid3
150. snnzg
151. snn0d
152. snnz
153. prnz
154. prnzg
155. tpnz
156. tpnzd
157. raltpd
158. snssb
159. snssg
160. snssgOLD
161. snss
162. eldifsn
163. eldifsnd
164. ssdifsn
165. elpwdifsn
166. eldifsni
167. eldifsnneq
168. neldifsn
169. neldifsnd
170. rexdifsn
171. raldifsni
172. raldifsnb
173. eldifvsn
174. difsn
175. difprsnss
176. difprsn1
177. difprsn2
178. diftpsn3
179. difpr
180. tpprceq3
181. tppreqb
182. difsnb
183. difsnpss
184. snssi
185. snssd
186. difsnid
187. eldifeldifsn
188. pw0
189. pwpw0
190. snsspr1
191. snsspr2
192. snsstp1
193. snsstp2
194. snsstp3
195. prssg
196. prss
197. prssi
198. prssd
199. prsspwg
200. ssprss
201. ssprsseq
202. sssn
203. ssunsn2
204. ssunsn
205. eqsn
206. eqsnd
207. eqsndOLD
208. issn
209. n0snor2el
210. ssunpr
211. sspr
212. sstp
213. tpss
214. tpssi
215. sneqrg
216. sneqr
217. snsssn
218. mosneq
219. sneqbg
220. snsspw
221. prsspw
222. preq1b
223. preq2b
224. preqr1
225. preqr2
226. preq12b
227. opthpr
228. preqr1g
229. preq12bg
230. prneimg
231. prneimg2
232. prnebg
233. pr1eqbg
234. pr1nebg
235. preqsnd
236. prnesn
237. prneprprc
238. preqsn
239. preq12nebg
240. prel12g
241. opthprneg
242. elpreqprlem
243. elpreqpr
244. elpreqprb
245. elpr2elpr
246. dfopif
247. dfopg
248. dfop
249. opeq1
250. opeq2
251. opeq12
252. opeq1i
253. opeq2i
254. opeq12i
255. opeq1d
256. opeq2d
257. opeq12d
258. oteq1
259. oteq2
260. oteq3
261. oteq1d
262. oteq2d
263. oteq3d
264. oteq123d
265. nfop
266. nfopd
267. csbopg
268. opidg
269. opid
270. ralunsn
271. 2ralunsn
272. opprc
273. opprc1
274. opprc2
275. oprcl
276. pwsn
277. pwpr
278. pwtp
279. pwpwpw0
280. pwv
281. prproe
282. 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. unieqi
14. unieqd
15. eluniab
16. elunirab
17. uniprg
18. unipr
19. unisng
20. unisn
21. unisnv
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. unissbOLD
35. uniss2
36. unidif
37. ssunieq
38. unimax
39. 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. elintabg
13. elintab
14. elintabOLD
15. elintrab
16. elintrabg
17. int0
18. intss1
19. ssint
20. ssintab
21. ssintub
22. ssmin
23. intmin
24. intss
25. intssuni
26. ssintrab
27. unissint
28. intssuni2
29. intminss
30. intmin2
31. intmin3
32. intmin4
33. intab
34. int0el
35. intun
36. intprg
37. intpr
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. eliund
9. iuncom
10. iuncom4
11. iunconst
12. iinconst
13. iuneqconst
14. iuniin
15. iinssiun
16. iunss1
17. iinss1
18. iuneq1
19. iineq1
20. ss2iun
21. iuneq2
22. iineq2
23. iuneq2i
24. iineq2i
25. iineq2d
26. iuneq2dv
27. iineq2dv
28. iuneq12df
29. iuneq1d
30. iuneq12dOLD
31. iuneq12d
32. iuneq2d
33. nfiun
34. nfiin
35. nfiung
36. nfiing
37. nfiu1
38. nfiu1OLD
39. nfii1
40. dfiun2g
41. dfiun2gOLD
42. dfiin2g
43. dfiun2
44. dfiin2
45. dfiunv2
46. cbviun
47. cbviin
48. cbviung
49. cbviing
50. cbviunv
51. cbviinv
52. cbviunvg
53. cbviinvg
54. iunssf
55. iunss
56. ssiun
57. ssiun2
58. ssiun2s
59. iunss2
60. iunssd
61. iunab
62. iunrab
63. iunxdif2
64. ssiinf
65. ssiin
66. iinss
67. iinss2
68. uniiun
69. intiin
70. iunid
71. iunidOLD
72. iun0
73. 0iun
74. 0iin
75. viin
76. iunsn
77. iunn0
78. iinab
79. iinrab
80. iinrab2
81. iunin2
82. iunin1
83. iinun2
84. iundif2
85. iindif1
86. 2iunin
87. iindif2
88. iinin2
89. iinin1
90. iinvdif
91. elriin
92. riin0
93. riinn0
94. riinrab
95. symdif0
96. symdifv
97. symdifid
98. iinxsng
99. iinxprg
100. iunxsng
101. iunxsn
102. iunxsngf
103. iunun
104. iunxun
105. iunxdif3
106. iunxprg
107. iunxiun
108. iinuni
109. iununi
110. sspwuni
111. pwssb
112. elpwpw
113. pwpwab
114. pwpwssunieq
115. elpwuni
116. iinpw
117. iunpwss
118. intss2
119. 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. invdisjrab
22. disjiun
23. disjord
24. disjiunb
25. disjiund
26. sndisj
27. 0disj
28. disjxsn
29. disjx0
30. disjprg
31. disjxiun
32. disjxun
33. 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. cbvopab1
14. cbvopab1g
15. cbvopab2
16. cbvopab1s
17. cbvopab1v
18. cbvopab1vOLD
19. cbvopab2v
20. unopab
Functions in maps-to notation
1. cmpt
2. df-mpt
3. mpteq12da
4. mpteq12df
5. mpteq12f
6. mpteq12dva
7. mpteq12dv
8. mpteq12
9. mpteq1
10. mpteq1d
11. mpteq1i
12. mpteq1iOLD
13. mpteq2da
14. mpteq2dva
15. mpteq2dv
16. mpteq2ia
17. mpteq2i
18. mpteq12i
19. nfmpt
20. nfmpt1
21. cbvmptf
22. cbvmptfg
23. cbvmpt
24. cbvmptg
25. cbvmptv
26. cbvmptvOLD
27. cbvmptvg
28. mptv
Transitive classes
1. wtr
2. df-tr
3. dftr2
4. dftr2c
5. dftr5
6. dftr5OLD
7. dftr3
8. dftr4
9. treq
10. trel
11. trel3
12. trss
13. trin
14. tr0
15. trv
16. triun
17. truni
18. triin
19. trint
20. trintss