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. elex22
27. prcnel
28. ralv
29. rexv
30. reuv
31. rmov
32. rabab
33. rexcom4b
34. ceqsal1t
35. ceqsalt
36. ceqsralt
37. ceqsalg
38. ceqsalgALT
39. ceqsal
40. ceqsalALT
41. ceqsalv
42. ceqsralv
43. gencl
44. 2gencl
45. 3gencl
46. cgsexg
47. cgsex2g
48. cgsex4g
49. cgsex4gOLD
50. ceqsex
51. ceqsexOLD
52. ceqsexv
53. ceqsexv2d
54. ceqsexv2dOLD
55. ceqsex2
56. ceqsex2v
57. ceqsex3v
58. ceqsex4v
59. ceqsex6v
60. ceqsex8v
61. gencbvex
62. gencbvex2
63. gencbval
64. sbhypf
65. sbhypfOLD
66. spcimgft
67. spcimgfi1
68. spcimgfi1OLD
69. spcgft
70. spcimgf
71. spcimegf
72. vtoclgft
73. vtocleg
74. vtoclg
75. vtocle
76. vtocleOLD
77. vtoclbg
78. vtocl
79. vtoclOLD
80. vtocldf
81. vtocld
82. vtocl2d
83. vtoclef
84. vtoclf
85. vtoclfOLD
86. vtocl2
87. vtocl3
88. vtoclb
89. vtoclgf
90. vtoclg1f
91. vtoclgOLD
92. vtocl2gf
93. vtocl3gf
94. vtocl2g
95. vtocl3g
96. vtoclgaf
97. vtoclga
98. vtocl2ga
99. vtocl2gaf
100. vtocl2gafOLD
101. vtocl3gaf
102. vtocl3gafOLD
103. vtocl3ga
104. vtocl3gaOLD
105. vtocl4g
106. vtocl4ga
107. vtocl4gaOLD
108. vtoclegft
109. vtoclegftOLD
110. vtoclri
111. spcgf
112. spcegf
113. spcimdv
114. spcdv
115. spcimedv
116. spcgv
117. spcegv
118. spcedv
119. spc2egv
120. spc2gv
121. spc2ed
122. spc2d
123. spc3egv
124. spc3gv
125. spcv
126. spcev
127. spc2ev
128. rspct
129. rspcdf
130. rspc
131. rspce
132. rspcimdv
133. rspcimedv
134. rspcdv
135. rspcedv
136. rspcebdv
137. rspcdv2
138. rspcv
139. rspccv
140. rspcva
141. rspccva
142. rspcev
143. rspcdva
144. rspcedvd
145. rspcedvdw
146. rspceb2dv
147. rspcime
148. rspceaimv
149. rspcedeq1vd
150. rspcedeq2vd
151. rspc2
152. rspc2gv
153. rspc2v
154. rspc2va
155. rspc2ev
156. 2rspcedvdw
157. rspc2dv
158. rspc3v
159. rspc3ev
160. 3rspcedvdw
161. rspc3dv
162. rspc4v
163. rspc6v
164. rspc8v
165. rspceeqv
166. ralxpxfr2d
167. rexraleqim
168. eqvincg
169. eqvinc
170. eqvincf
171. alexeqg
172. ceqex
173. ceqsexg
174. ceqsexgv
175. ceqsrexv
176. ceqsrexbv
177. ceqsralbv
178. ceqsrex2v
179. clel2g
180. clel2
181. clel3g
182. clel3
183. clel4g
184. clel4
185. clel5
186. pm13.183
187. rr19.3v
188. rr19.28v
189. elab6g
190. elabd2
191. elabd3
192. elabgt
193. elabgtOLD
194. elabgtOLDOLD
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. elrab3t
212. elrab
213. elrab3
214. elrabd
215. elrab2
216. elrab2w
217. ralab
218. ralrab
219. rexab
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
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. abssi
103. ss2rab
104. rabss
105. ssrab
106. ssrabdv
107. rabssdv
108. ss2rabdv
109. ss2rabi
110. rabss2
111. ssab2
112. ssrab2
113. rabss3d
114. ssrab3
115. rabssrabd
116. ssrabeq
117. rabssab
118. eqrrabd
119. uniiunlem
120. dfpss2
121. dfpss3
122. psseq1
123. psseq2
124. psseq1i
125. psseq2i
126. psseq12i
127. psseq1d
128. psseq2d
129. psseq12d
130. pssss
131. pssne
132. pssssd
133. pssned
134. sspss
135. pssirr
136. pssn2lp
137. sspsstri
138. ssnpss
139. psstr
140. sspsstr
141. psssstr
142. psstrd
143. sspsstrd
144. psssstrd
145. npss
146. ssnelpss
147. ssnelpssd
148. 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. 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. eldifsn
165. eldifsnd
166. ssdifsn
167. elpwdifsn
168. eldifsni
169. eldifsnneq
170. neldifsn
171. neldifsnd
172. rexdifsn
173. raldifsni
174. raldifsnb
175. eldifvsn
176. difsn
177. difprsnss
178. difprsn1
179. difprsn2
180. diftpsn3
181. difpr
182. tpprceq3
183. tppreqb
184. difsnb
185. difsnpss
186. snssi
187. snssd
188. difsnid
189. eldifeldifsn
190. pw0
191. pwpw0
192. snsspr1
193. snsspr2
194. snsstp1
195. snsstp2
196. snsstp3
197. prssg
198. prss
199. prssi
200. prssd
201. prsspwg
202. ssprss
203. ssprsseq
204. sssn
205. ssunsn2
206. ssunsn
207. eqsn
208. eqsnd
209. eqsndOLD
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. 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. 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. nfiu1OLD
39. nfii1
40. dfiun2g
41. dfiin2g
42. dfiun2
43. dfiin2
44. dfiunv2
45. cbviun
46. cbviin
47. cbviung
48. cbviing
49. cbviunv
50. cbviinv
51. cbviunvg
52. cbviinvg
53. iunssf
54. iunss
55. ssiun
56. ssiun2
57. ssiun2s
58. iunss2
59. iunssd
60. iunab
61. iunrab
62. iunxdif2
63. ssiinf
64. ssiin
65. iinss
66. iinss2
67. uniiun
68. intiin
69. iunid
70. iun0
71. 0iun
72. 0iin
73. viin
74. iunsn
75. iunn0
76. iinab
77. iinrab
78. iinrab2
79. iunin2
80. iunin1
81. iinun2
82. iundif2
83. iindif1
84. 2iunin
85. iindif2
86. iinin2
87. iinin1
88. iinvdif
89. elriin
90. riin0
91. riinn0
92. riinrab
93. symdif0
94. symdifv
95. symdifid
96. iinxsng
97. iinxprg
98. iunxsng
99. iunxsn
100. iunxsngf
101. iunun
102. iunxun
103. iunxdif3
104. iunxprg
105. iunxiun
106. iinuni
107. iununi
108. sspwuni
109. pwssb
110. elpwpw
111. pwpwab
112. pwpwssunieq
113. elpwuni
114. iinpw
115. iunpwss
116. intss2
117. 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. 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. trin
13. tr0
14. trv
15. triun
16. truni
17. triin
18. trint
19. trintss