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. eqabf
54. abid2f
55. abid2fOLD
56. sbabel
57. sbabelOLD
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. vexOLD
7. elv
8. elvd
9. el2v
10. eqv
11. eqvf
12. abv
13. abvALT
14. isset
15. issetft
16. issetf
17. isseti
18. issetri
19. eqvisset
20. elex
21. elexi
22. elexd
23. elex2OLD
24. elex22
25. prcnel
26. ralv
27. rexv
28. reuv
29. rmov
30. rabab
31. rexcom4b
32. ceqsal1t
33. ceqsalt
34. ceqsralt
35. ceqsalg
36. ceqsalgALT
37. ceqsal
38. ceqsalALT
39. ceqsalv
40. ceqsalvOLD
41. ceqsralv
42. ceqsralvOLD
43. gencl
44. 2gencl
45. 3gencl
46. cgsexg
47. cgsex2g
48. cgsex4g
49. cgsex4gOLD
50. cgsex4gOLDOLD
51. ceqsex
52. ceqsexOLD
53. ceqsexv
54. ceqsexvOLD
55. ceqsexvOLDOLD
56. ceqsexv2d
57. ceqsex2
58. ceqsex2v
59. ceqsex3v
60. ceqsex4v
61. ceqsex6v
62. ceqsex8v
63. gencbvex
64. gencbvex2
65. gencbval
66. sbhypf
67. sbhypfOLD
68. vtoclgft
69. vtocleg
70. vtoclg
71. vtocle
72. vtoclbg
73. vtocl
74. vtocldf
75. vtocld
76. vtocldOLD
77. vtocl2d
78. vtoclef
79. vtoclf
80. vtoclfOLD
81. vtoclALT
82. vtocl2
83. vtocl3
84. vtoclb
85. vtoclgf
86. vtoclg1f
87. vtoclgOLD
88. vtoclgOLDOLD
89. vtocl2gf
90. vtocl3gf
91. vtocl2g
92. vtocl3g
93. vtoclgaf
94. vtoclga
95. vtocl2ga
96. vtocl2gaf
97. vtocl3gaf
98. vtocl3ga
99. vtocl3gaOLD
100. vtocl4g
101. vtocl4ga
102. vtoclegft
103. vtoclegftOLD
104. vtoclri
105. spcimgft
106. spcgft
107. spcimgf
108. spcimegf
109. spcgf
110. spcegf
111. spcimdv
112. spcdv
113. spcimedv
114. spcgv
115. spcegv
116. spcedv
117. spc2egv
118. spc2gv
119. spc2ed
120. spc2d
121. spc3egv
122. spc3gv
123. spcv
124. spcev
125. spc2ev
126. rspct
127. rspcdf
128. rspc
129. rspce
130. rspcimdv
131. rspcimedv
132. rspcdv
133. rspcedv
134. rspcebdv
135. rspcdv2
136. rspcv
137. rspccv
138. rspcva
139. rspccva
140. rspcev
141. rspcdva
142. rspcedvd
143. rspcedvdw
144. rspcime
145. rspceaimv
146. rspcedeq1vd
147. rspcedeq2vd
148. rspc2
149. rspc2gv
150. rspc2v
151. rspc2va
152. rspc2ev
153. 2rspcedvdw
154. rspc2dv
155. rspc3v
156. rspc3ev
157. rspc3dv
158. rspc4v
159. rspc6v
160. rspc8v
161. rspceeqv
162. ralxpxfr2d
163. rexraleqim
164. eqvincg
165. eqvinc
166. eqvincf
167. alexeqg
168. ceqex
169. ceqsexg
170. ceqsexgv
171. ceqsrexv
172. ceqsrexbv
173. ceqsralbv
174. ceqsrex2v
175. clel2g
176. clel2gOLD
177. clel2
178. clel3g
179. clel3
180. clel4g
181. clel4
182. clel4OLD
183. clel5
184. pm13.183
185. rr19.3v
186. rr19.28v
187. elab6g
188. elabd2
189. elabd3
190. elabgt
191. elabgtOLD
192. elabgf
193. elabf
194. elabg
195. elabgOLD
196. elab
197. elabOLD
198. elab2g
199. elabd
200. elab2
201. elab4g
202. elab3gf
203. elab3g
204. elab3
205. elrabi
206. elrabiOLD
207. elrabf
208. rabtru
209. rabeqcOLD
210. elrab3t
211. elrab
212. elrab3
213. elrabd
214. elrab2
215. ralab
216. ralabOLD
217. ralrab
218. rexab
219. rexabOLD
220. rexrab
221. ralab2
222. ralrab2
223. rexab2
224. rexrab2
225. reurab
226. abidnf
227. dedhb
228. class2seteq
229. nelrdva
230. eqeu
231. moeq
232. eueq
233. eueqi
234. eueq2
235. eueq3
236. moeq3
237. mosub
238. mo2icl
239. mob2
240. moi2
241. mob
242. moi
243. morex
244. euxfr2w
245. euxfrw
246. euxfr2
247. euxfr
248. euind
249. reu2
250. reu6
251. reu3
252. reu6i
253. eqreu
254. rmo4
255. reu4
256. reu7
257. reu8
258. rmo3f
259. rmo4f
260. reu2eqd
261. reueq
262. rmoeq
263. rmoan
264. rmoim
265. rmoimia
266. rmoimi
267. rmoimi2
268. 2reu5a
269. reuimrmo
270. 2reuswap
271. 2reuswap2
272. reuxfrd
273. reuxfr
274. reuxfr1d
275. reuxfr1ds
276. reuxfr1
277. reuind
278. 2rmorex
279. 2reu5lem1
280. 2reu5lem2
281. 2reu5lem3
282. 2reu5
283. 2reurmo
284. 2reurex
285. 2rmoswap
286. 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. sbcbii
62. sbcbi1
63. sbcbi2
64. sbcbi2OLD
65. sbcal
66. sbcex2
67. sbceqal
68. sbceqalOLD
69. sbeqalb
70. eqsbc2
71. sbc3an
72. sbcel1v
73. sbcel2gv
74. sbcel21v
75. sbcimdv
76. sbcimdvOLD
77. sbctt
78. sbcgf
79. sbc19.21g
80. sbcg
81. sbcgOLD
82. sbcgfi
83. sbc2iegf
84. sbc2ie
85. sbc2ieOLD
86. sbc2iedv
87. sbc3ie
88. sbccomlem
89. sbccom
90. sbcralt
91. sbcrext
92. sbcralg
93. sbcrex
94. sbcreu
95. reu8nf
96. sbcabel
97. rspsbc
98. rspsbca
99. rspesbca
100. spesbc
101. spesbcd
102. sbcth2
103. ra4v
104. ra4
105. rmo2
106. rmo2i
107. rmo3
108. rmob
109. rmoi
110. rmob2
111. rmoi2
112. rmoanim
113. rmoanimALT
114. reuan
115. 2reu1
116. 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. eqimssd
75. eqimsscd
76. eqimss
77. eqimss2
78. eqimssi
79. eqimss2i
80. nssne1
81. nssne2
82. nss
83. nelss
84. ssrexf
85. ssrmof
86. ssralv
87. ssrexv
88. ss2ralv
89. ss2rexv
90. ralss
91. rexss
92. ss2ab
93. abss
94. ssab
95. ssabral
96. ss2abdv
97. ss2abdvALT
98. ss2abdvOLD
99. ss2abi
100. ss2abiOLD
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. ssrab2OLD
115. rabss3d
116. ssrab3
117. rabssrabd
118. ssrabeq
119. rabssab
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. 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. undifr
162. undifrOLD
163. undif5
164. ssdifin0
165. ssdifeq0
166. ssundif
167. difcom
168. pssdifcom1
169. pssdifcom2
170. difdifdir
171. uneqdifeq
172. raldifeq
173. r19.2z
174. r19.2zb
175. r19.3rz
176. r19.28z
177. r19.3rzv
178. r19.9rzv
179. r19.28zv
180. r19.37zv
181. r19.45zv
182. r19.44zv
183. r19.27z
184. r19.27zv
185. r19.36zv
186. ralidmw
187. rzal
188. rzalALT
189. rexn0
190. ralidm
191. ral0
192. ralf0
193. rexn0OLD
194. ralidmOLD
195. ral0OLD
196. ralf0OLD
197. ralnralall
198. falseral0
199. raaan
200. raaanv
201. sbss
202. sbcssg
203. raaan2
204. 2reu4lem
205. 2reu4
206. 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. 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. 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. rabeqsnd
46. ralsnsg
47. rexsns
48. rexsngf
49. ralsngf
50. reusngf
51. ralsng
52. rexsng
53. reusng
54. 2ralsng
55. ralsngOLD
56. rexsngOLD
57. rexreusng
58. exsnrex
59. ralsn
60. rexsn
61. elpwunsn
62. eqoreldif
63. eltpg
64. eldiftp
65. eltpi
66. eltp
67. dftp2
68. nfpr
69. ifpr
70. ralprgf
71. rexprgf
72. ralprg
73. ralprgOLD
74. rexprg
75. rexprgOLD
76. raltpg
77. rextpg
78. ralpr
79. rexpr
80. reuprg0
81. reuprg
82. reurexprg
83. raltp
84. rextp
85. nfsn
86. csbsng
87. csbprg
88. elinsn
89. disjsn
90. disjsn2
91. disjpr2
92. disjprsn
93. disjtpsn
94. disjtp2
95. snprc
96. snnzb
97. rmosn
98. r19.12sn
99. rabsn
100. rabsnifsb
101. rabsnif
102. rabrsn
103. euabsn2
104. euabsn
105. reusn
106. absneu
107. rabsneu
108. eusn
109. rabsnt
110. prcom
111. preq1
112. preq2
113. preq12
114. preq1i
115. preq2i
116. preq12i
117. preq1d
118. preq2d
119. preq12d
120. tpeq1
121. tpeq2
122. tpeq3
123. tpeq1d
124. tpeq2d
125. tpeq3d
126. tpeq123d
127. tprot
128. tpcoma
129. tpcomb
130. tpass
131. qdass
132. qdassr
133. tpidm12
134. tpidm13
135. tpidm23
136. tpidm
137. tppreq3
138. prid1g
139. prid2g
140. prid1
141. prid2
142. ifpprsnss
143. prprc1
144. prprc2
145. prprc
146. tpid1
147. tpid1g
148. tpid2
149. tpid2g
150. tpid3g
151. tpid3
152. snnzg
153. snn0d
154. snnz
155. prnz
156. prnzg
157. tpnz
158. tpnzd
159. raltpd
160. snssb
161. snssg
162. snssgOLD
163. snss
164. eldifsn
165. ssdifsn
166. elpwdifsn
167. eldifsni
168. eldifsnneq
169. neldifsn
170. neldifsnd
171. rexdifsn
172. raldifsni
173. raldifsnb
174. eldifvsn
175. difsn
176. difprsnss
177. difprsn1
178. difprsn2
179. diftpsn3
180. difpr
181. tpprceq3
182. tppreqb
183. difsnb
184. difsnpss
185. snssi
186. snssd
187. difsnid
188. eldifeldifsn
189. pw0
190. pwpw0
191. snsspr1
192. snsspr2
193. snsstp1
194. snsstp2
195. snsstp3
196. prssg
197. prss
198. prssi
199. prssd
200. prsspwg
201. ssprss
202. ssprsseq
203. sssn
204. ssunsn2
205. ssunsn
206. eqsn
207. issn
208. n0snor2el
209. ssunpr
210. sspr
211. sstp
212. tpss
213. tpssi
214. sneqrg
215. sneqr
216. snsssn
217. mosneq
218. sneqbg
219. snsspw
220. prsspw
221. preq1b
222. preq2b
223. preqr1
224. preqr2
225. preq12b
226. opthpr
227. preqr1g
228. preq12bg
229. prneimg
230. prnebg
231. pr1eqbg
232. pr1nebg
233. preqsnd
234. prnesn
235. prneprprc
236. preqsn
237. preq12nebg
238. prel12g
239. opthprneg
240. elpreqprlem
241. elpreqpr
242. elpreqprb
243. elpr2elpr
244. dfopif
245. dfopg
246. dfop
247. opeq1
248. opeq2
249. opeq12
250. opeq1i
251. opeq2i
252. opeq12i
253. opeq1d
254. opeq2d
255. opeq12d
256. oteq1
257. oteq2
258. oteq3
259. oteq1d
260. oteq2d
261. oteq3d
262. oteq123d
263. nfop
264. nfopd
265. csbopg
266. opidg
267. opid
268. ralunsn
269. 2ralunsn
270. opprc
271. opprc1
272. opprc2
273. oprcl
274. pwsn
275. pwsnOLD
276. pwpr
277. pwtp
278. pwpwpw0
279. pwv
280. prproe
281. 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. unisnv
25. unisn3
26. dfnfc2
27. uniun
28. uniin
29. ssuni
30. uni0b
31. uni0c
32. uni0
33. csbuni
34. elssuni
35. unissel
36. unissb
37. unissbOLD
38. uniss2
39. unidif
40. ssunieq
41. unimax
42. 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. intprOLD
39. intprgOLD
40. intsng
41. intsn
42. uniintsn
43. uniintab
44. intunsn
45. rint0
46. elrint
47. 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. iunidOLD
69. iun0
70. 0iun
71. 0iin
72. viin
73. iunsn
74. iunn0
75. iinab
76. iinrab
77. iinrab2
78. iunin2
79. iunin1
80. iinun2
81. iundif2
82. iindif1
83. 2iunin
84. iindif2
85. iinin2
86. iinin1
87. iinvdif
88. elriin
89. riin0
90. riinn0
91. riinrab
92. symdif0
93. symdifv
94. symdifid
95. iinxsng
96. iinxprg
97. iunxsng
98. iunxsn
99. iunxsngf
100. iunun
101. iunxun
102. iunxdif3
103. iunxprg
104. iunxiun
105. iinuni
106. iununi
107. sspwuni
108. pwssb
109. elpwpw
110. pwpwab
111. pwpwssunieq
112. elpwuni
113. iinpw
114. iunpwss
115. intss2
116. 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. 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