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. nfaba1g
26. nfeqd
27. nfeld
28. nfnfc
29. nfeq
30. nfel
31. nfeq1
32. nfel1
33. nfeq2
34. nfel2
35. drnfc1
36. drnfc2
37. nfabdw
38. nfabd
39. nfabd2
40. dvelimdc
41. dvelimc
42. nfcvf
43. nfcvf2
44. cleqf
45. eqabf
46. abid2f
47. abid2fOLD
48. 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. elexi
24. elexd
25. elex22
26. prcnel
27. ralv
28. rexv
29. reuv
30. rmov
31. rabab
32. rexcom4b
33. ceqsal1t
34. ceqsalt
35. ceqsralt
36. ceqsalg
37. ceqsalgALT
38. ceqsal
39. ceqsalALT
40. ceqsalv
41. ceqsralv
42. gencl
43. 2gencl
44. 3gencl
45. cgsexg
46. cgsex2g
47. cgsex4g
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. spcimgft
62. spcimgfi1
63. spcimgfi1OLD
64. spcgft
65. spcimgf
66. spcimegf
67. vtoclgft
68. vtocleg
69. vtoclg
70. vtocle
71. vtoclbg
72. vtocl
73. vtocldf
74. vtocld
75. vtocl2d
76. vtoclef
77. vtoclf
78. vtocl2
79. vtocl3
80. vtoclb
81. vtoclgf
82. vtoclg1f
83. vtocl2gf
84. vtocl3gf
85. vtocl2g
86. vtocl3g
87. vtoclgaf
88. vtoclga
89. vtocl2ga
90. vtocl2gaf
91. vtocl3gaf
92. vtocl3ga
93. vtocl4g
94. vtocl4ga
95. vtoclegft
96. vtoclri
97. spcgf
98. spcegf
99. spcimdv
100. spcdv
101. spcimedv
102. spcgv
103. spcegv
104. spcedv
105. spc2egv
106. spc2gv
107. spc2ed
108. spc2d
109. spc3egv
110. spc3gv
111. spcv
112. spcev
113. spc2ev
114. rspct
115. rspcdf
116. rspc
117. rspce
118. rspcimdv
119. rspcimedv
120. rspcdv
121. rspcedv
122. rspcebdv
123. rspcdv2
124. rspcv
125. rspccv
126. rspcva
127. rspccva
128. rspcev
129. rspcdva
130. rspcedvd
131. rspcedvdw
132. rspceb2dv
133. rspcime
134. rspceaimv
135. rspcedeq1vd
136. rspcedeq2vd
137. rspc2
138. rspc2gv
139. rspc2v
140. rspc2va
141. rspc2ev
142. 2rspcedvdw
143. rspc2dv
144. rspc3v
145. rspc3ev
146. 3rspcedvdw
147. rspc3dv
148. rspc4v
149. rspc6v
150. rspc8v
151. rspceeqv
152. ralxpxfr2d
153. rexraleqim
154. eqvincg
155. eqvinc
156. eqvincf
157. alexeqg
158. ceqex
159. ceqsexg
160. ceqsexgv
161. ceqsrexv
162. ceqsrexbv
163. ceqsralbv
164. ceqsrex2v
165. clel2g
166. clel2
167. clel3g
168. clel3
169. clel4g
170. clel4
171. clel5
172. pm13.183
173. rr19.3v
174. rr19.28v
175. elab6g
176. elabd2
177. elabd3
178. elabgt
179. elabgtOLD
180. elabgf
181. elabf
182. elabg
183. elabgw
184. elab2gw
185. elab
186. elab2g
187. elabd
188. elab2
189. elab4g
190. elab3gf
191. elab3g
192. elab3
193. elrabi
194. elrabf
195. rabtru
196. elrab3t
197. elrab
198. elrab3
199. elrabd
200. elrabrd
201. elrab2
202. elrab2w
203. ralab
204. ralrab
205. rexab
206. rexrab
207. ralab2
208. ralrab2
209. rexab2
210. rexrab2
211. reurab
212. abidnf
213. dedhb
214. class2seteq
215. nelrdva
216. eqeu
217. moeq
218. eueq
219. eueqi
220. eueq2
221. eueq3
222. moeq3
223. mosub
224. mo2icl
225. mob2
226. moi2
227. mob
228. moi
229. morex
230. euxfr2w
231. euxfrw
232. euxfr2
233. euxfr
234. euind
235. reu2
236. reu6
237. reu3
238. reu6i
239. eqreu
240. rmo4
241. reu4
242. reu7
243. reu8
244. rmo3f
245. rmo4f
246. reu2eqd
247. reueq
248. rmoeq
249. rmoan
250. rmoim
251. rmoimia
252. rmoimi
253. rmoimi2
254. 2reu5a
255. reuimrmo
256. 2reuswap
257. 2reuswap2
258. reuxfrd
259. reuxfr
260. reuxfr1d
261. reuxfr1ds
262. reuxfr1
263. reuind
264. 2rmorex
265. 2reu5lem1
266. 2reu5lem2
267. 2reu5lem3
268. 2reu5
269. 2reurmo
270. 2reurex
271. 2rmoswap
272. 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. sbc6
33. sbc7
34. cbvsbcw
35. cbvsbcvw
36. cbvsbc
37. cbvsbcv
38. sbciegft
39. sbciegf
40. sbcieg
41. sbcie2g
42. sbcie
43. sbciedf
44. sbcied
45. sbcied2
46. elrabsf
47. eqsbc1
48. sbcng
49. sbcimg
50. sbcan
51. sbcor
52. sbcbig
53. sbcn1
54. sbcim1
55. sbcbid
56. sbcbidv
57. sbcbii
58. sbcbi1
59. sbcbi2
60. sbcal
61. sbcex2
62. sbceqal
63. sbeqalb
64. eqsbc2
65. sbc3an
66. sbcel1v
67. sbcel2gv
68. sbcel21v
69. sbcimdv
70. sbctt
71. sbcgf
72. sbc19.21g
73. sbcg
74. sbcgfi
75. sbc2iegf
76. sbc2ie
77. sbc2iedv
78. sbc3ie
79. sbccomlem
80. sbccomlemOLD
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. nrmod
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. 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. eqsstrd
51. eqsstrrd
52. sseqtrd
53. sseqtrrd
54. eqsstrid
55. eqsstrrid
56. sseqtrdi
57. sseqtrrdi
58. sseqtrid
59. sseqtrrid
60. eqsstrdi
61. eqsstrrdi
62. eqsstri
63. eqsstrri
64. sseqtri
65. sseqtrri
66. 3sstr3i
67. 3sstr4i
68. 3sstr3g
69. 3sstr4g
70. 3sstr3d
71. 3sstr4d
72. eqimssd
73. eqimsscd
74. eqimss
75. eqimss2
76. eqimssi
77. eqimss2i
78. nssne1
79. nssne2
80. nss
81. nssrex
82. nelss
83. ssrexf
84. ssrmof
85. ssralv
86. ssrexv
87. ss2ralv
88. ss2rexv
89. ralss
90. rexss
91. ralssOLD
92. rexssOLD
93. ss2abim
94. ss2ab
95. abss
96. ssab
97. ssabral
98. ss2abdv
99. ss2abi
100. abssdv
101. abssi
102. ss2rab
103. rabss
104. ssrab
105. ss2rabd
106. ssrabdv
107. rabssdv
108. ss2rabdv
109. ss2rabi
110. rabss2
111. rabss2OLD
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. pssirrOLD
138. pssn2lp
139. sspsstri
140. ssnpss
141. psstr
142. sspsstr
143. psssstr
144. psstrd
145. sspsstrd
146. psssstrd
147. npss
148. ssnelpss
149. ssnelpssd
150. 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. vn0OLD
15. vn0ALT
16. eq0f
17. neq0f
18. n0f
19. eq0
20. eq0ALT
21. neq0
22. n0
23. n0limd
24. nel0
25. reximdva0
26. rspn0
27. n0rex
28. ssn0rex
29. n0moeu
30. rex0
31. reu0
32. rmo0
33. 0el
34. n0el
35. eqeuel
36. ssdif0
37. difn0
38. pssdifn0
39. pssdif
40. ndisj
41. inn0f
42. inn0
43. difin0ss
44. inssdif0
45. inssdif0OLD
46. inindif
47. difid
48. difidALT
49. dif0
50. ab0w
51. ab0
52. ab0ALT
53. dfnf5
54. ab0orv
55. ab0orvALT
56. abn0
57. rab0
58. rab0OLD
59. rabeq0w
60. rabeq0
61. rabn0
62. rabxm
63. rabnc
64. elneldisj
65. elnelun
66. un0
67. in0
68. 0un
69. 0in
70. inv1
71. unv
72. 0ss
73. ss0b
74. ss0
75. sseq0b
76. sseq0
77. ssn0
78. 0dif
79. un00
80. vss
81. vvin
82. 0pss
83. npss0
84. pssv
85. nvpss
86. abf
87. eq0rdv
88. eq0rdvALT
89. csbprc
90. csb0
91. sbcel12
92. sbceqg
93. sbceqi
94. sbcnel12g
95. sbcne12
96. sbcel1g
97. sbceq1g
98. sbcel2
99. sbceq2g
100. csbcom
101. sbcnestgfw
102. csbnestgfw
103. sbcnestgw
104. csbnestgw
105. sbcco3gw
106. sbcnestgf
107. csbnestgf
108. sbcnestg
109. csbnestg
110. sbcco3g
111. csbco3g
112. csbnest1g
113. csbidm
114. csbvarg
115. csbvargi
116. sbccsb
117. sbccsb2
118. rspcsbela
119. sbnfc2
120. csbab
121. csbun
122. csbin
123. csbie2df
124. 2nreu
125. disj
126. disjr
127. disj1
128. reldisj
129. disj3
130. disjne
131. disjeq0
132. disjel
133. disj2
134. disj4
135. ssdisj
136. disjpss
137. undisj1
138. undisj2
139. ssindif0
140. inelcm
141. minel
142. undif4
143. disjssun
144. vdif0
145. difrab0eq
146. pssnel
147. disjdifg
148. disjdif
149. disjdifr
150. difin0
151. unvdif
152. undif1
153. undif2
154. undifabs
155. inundif
156. disjdif2
157. difun2
158. undif
159. undifr
160. undif5
161. ssdifin0
162. ssdifeq0
163. ssundif
164. difcom
165. pssdifcom1
166. pssdifcom2
167. difdifdir
168. uneqdifeq
169. raldifeq
170. rzal
171. rzalALT
172. rexn0
173. ralf0
174. ral0
175. r19.2z
176. r19.2zb
177. r19.3rz
178. r19.28z
179. r19.3rzv
180. r19.3rzvOLD
181. r19.9rzv
182. r19.28zv
183. r19.37zv
184. r19.45zv
185. r19.44zv
186. r19.27z
187. r19.27zv
188. r19.36zv
189. ralnralall
190. falseral0
191. falseral0OLD
192. ralidmw
193. ralidm
194. raaan
195. raaanv
196. sbss
197. sbcssg
198. raaan2
199. 2reu4lem
200. 2reu4
201. 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. pwidgOLD
23. pwidb
24. pwid
25. pwss
26. 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. elsnd
21. rabsneq
22. absn
23. dfpr2
24. dfsn2ALT
25. elprg
26. elpri
27. elpr
28. elpr2g
29. elpr2
30. elprn1
31. elprn2
32. nelpr2
33. nelpr1
34. nelpri
35. prneli
36. nelprd
37. eldifpr
38. rexdifpr
39. snidg
40. snidb
41. snid
42. vsnid
43. elsn2g
44. elsn2
45. nelsn
46. rabeqsn
47. rabsssn
48. rabeqsnd
49. ralsnsg
50. rexsns
51. rexsngf
52. ralsngf
53. reusngf
54. ralsng
55. rexsng
56. reusng
57. 2ralsng
58. rexreusng
59. exsnrex
60. ralsn
61. rexsn
62. elunsn
63. elpwunsn
64. eqoreldif
65. eltpg
66. eldiftp
67. eltpi
68. eltp
69. el7g
70. dftp2
71. nfpr
72. ifpr
73. ralprgf
74. rexprgf
75. ralprg
76. rexprg
77. raltpg
78. rextpg
79. ralpr
80. rexpr
81. reuprg0
82. reuprg
83. reurexprg
84. raltp
85. rextp
86. nfsn
87. csbsng
88. csbprg
89. elinsn
90. disjsn
91. disjsn2
92. disjpr2
93. disjprsn
94. disjtpsn
95. disjtp2
96. snprc
97. snnzb
98. rmosn
99. r19.12sn
100. rabsn
101. rabsnifsb
102. rabsnif
103. rabrsn
104. euabsn2
105. euabsn
106. reusn
107. absneu
108. rabsneu
109. eusn
110. rabsnt
111. prcom
112. preq1
113. preq2
114. preq12
115. preq1i
116. preq2i
117. preq12i
118. preq1d
119. preq2d
120. preq12d
121. tpeq1
122. tpeq2
123. tpeq3
124. tpeq1d
125. tpeq2d
126. tpeq3d
127. tpeq123d
128. tprot
129. tpcoma
130. tpcomb
131. tpass
132. qdass
133. qdassr
134. tpidm12
135. tpidm13
136. tpidm23
137. tpidm
138. tppreq3
139. prid1g
140. prid2g
141. prid1
142. prid2
143. ifpprsnss
144. prprc1
145. prprc2
146. prprc
147. tpid1
148. tpid1g
149. tpid2
150. tpid2g
151. tpid3g
152. tpid3
153. snnzg
154. snn0d
155. snnz
156. prnz
157. prnzg
158. tpnz
159. tpnzd
160. raltpd
161. snssb
162. snssg
163. snss
164. snssi
165. snssd
166. eldifsn
167. eldifsnbd
168. eldifsnd
169. ssdifsn
170. elpwdifsn
171. eldifsni
172. eldifsnneq
173. neldifsn
174. neldifsnd
175. rexdifsn
176. raldifsni
177. raldifsnb
178. eldifvsn
179. difsn
180. difprsnss
181. difprsn1
182. difprsn2
183. diftpsn3
184. difpr
185. tpprceq3
186. tppreqb
187. difsnb
188. difsnpss
189. difsnid
190. eldifeldifsn
191. pw0
192. pwpw0
193. snsspr1
194. snsspr2
195. snsstp1
196. snsstp2
197. snsstp3
198. prssg
199. prss
200. prssi
201. prssd
202. prsspwg
203. ssprss
204. ssprsseq
205. sssn
206. ssunsn2
207. ssunsn
208. eqsn
209. eqsnd
210. issn
211. n0snor2el
212. ssunpr
213. sspr
214. sstp
215. tpss
216. tpssi
217. sneqrg
218. sneqr
219. snsssn
220. mosneq
221. sneqbg
222. snsspw
223. prsspw
224. preq1b
225. preq2b
226. preqr1
227. preqr2
228. preq12b
229. opthpr
230. preqr1g
231. preq12bg
232. prneimg
233. prneimg2
234. prnebg
235. pr1eqbg
236. pr1nebg
237. preqsnd
238. prnesn
239. prneprprc
240. preqsn
241. preq12nebg
242. prel12g
243. opthprneg
244. elpreqprlem
245. elpreqpr
246. elpreqprb
247. elpr2elpr
248. dfopif
249. dfopg
250. dfop
251. opeq1
252. opeq2
253. opeq12
254. opeq1i
255. opeq2i
256. opeq12i
257. opeq1d
258. opeq2d
259. opeq12d
260. oteq1
261. oteq2
262. oteq3
263. oteq1d
264. oteq2d
265. oteq3d
266. oteq123d
267. nfop
268. nfopd
269. csbopg
270. opidg
271. opid
272. ralunsn
273. 2ralunsn
274. opprc
275. opprc1
276. opprc2
277. oprcl
278. pwsn
279. pwpr
280. pwtp
281. pwpwpw0
282. pwv
283. prproe
284. 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. uniinOLD
27. ssuni
28. uni0b
29. uni0c
30. uni0
31. uni0OLD
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. elintabg
13. elintab
14. elintrab
15. elintrabg
16. int0
17. intss1
18. ssint
19. ssintab
20. ssintub
21. ssmin
22. intmin
23. intss
24. intssuni
25. ssintrab
26. unissint
27. intssuni2
28. intminss
29. intmin2
30. intmin3
31. intmin4
32. intab
33. int0el
34. intun
35. intprg
36. intpr
37. intsng
38. intsn
39. uniintsn
40. uniintab
41. intunsn
42. rint0
43. elrint
44. 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. nfii1
39. dfiun2g
40. dfiin2g
41. dfiun2
42. dfiin2
43. dfiunv2
44. cbviun
45. cbviin
46. cbviung
47. cbviing
48. cbviunv
49. cbviinv
50. cbviunvg
51. cbviinvg
52. iunssf
53. iunssfOLD
54. iunss
55. iunssOLD
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. iun0
72. 0iun
73. 0iin
74. viin
75. iunsn
76. iunn0
77. iinab
78. iinrab
79. iinrab2
80. iunin2
81. iunin1
82. iinun2
83. iundif2
84. uniin1
85. uniin2
86. iindif1
87. 2iunin
88. iindif2
89. iinin2
90. iinin1
91. iinvdif
92. elriin
93. riin0
94. riinn0
95. riinrab
96. symdif0
97. symdifv
98. symdifid
99. iinxsng
100. iinxprg
101. iunxsng
102. iunxsn
103. iunxsngf
104. iunun
105. iunxun
106. iunxdif3
107. iunxprg
108. iunxiun
109. iinuni
110. iununi
111. sspwuni
112. pwssb
113. elpwpw
114. pwpwab
115. pwpwssunieq
116. elpwuni
117. iinpw
118. iunpwss
119. intss2
120. 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. breq1dd
20. breq2dd
21. eqnbrtrd
22. nbrne1
23. nbrne2
24. eqbrtri
25. eqbrtrd
26. eqbrtrri
27. eqbrtrrd
28. breqtri
29. breqtrd
30. breqtrri
31. breqtrrd
32. 3brtr3i
33. 3brtr4i
34. 3brtr3d
35. 3brtr4d
36. 3brtr3g
37. 3brtr4g
38. eqbrtrid
39. eqbrtrrid
40. breqtrid
41. breqtrrid
42. eqbrtrdi
43. eqbrtrrdi
44. breqtrdi
45. breqtrrdi
46. ssbrd
47. ssbr
48. ssbri
49. nfbrd
50. nfbr
51. brab1
52. br0
53. brne0
54. brun
55. brin
56. brdif
57. sbcbr123
58. sbcbr
59. sbcbr12g
60. sbcbr1g
61. sbcbr2g
62. brsymdif
63. brralrspcev
64. 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. cbvopab2v
19. 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. mpteq2da
13. mpteq2dva
14. mpteq2dv
15. mpteq2ia
16. mpteq2i
17. mpteq12i
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. dftr2c
5. dftr5
6. dftr3
7. dftr4
8. treq
9. trel
10. trel3
11. trss
12. trun
13. trin
14. tr0
15. trv
16. triun
17. truni
18. triin
19. trint
20. trintss