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. 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. 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. nelpr2
31. nelpr1
32. nelpri
33. prneli
34. nelprd
35. eldifpr
36. rexdifpr
37. snidg
38. snidb
39. snid
40. vsnid
41. elsn2g
42. elsn2
43. nelsn
44. rabeqsn
45. rabsssn
46. rabeqsnd
47. ralsnsg
48. rexsns
49. rexsngf
50. ralsngf
51. reusngf
52. ralsng
53. rexsng
54. reusng
55. 2ralsng
56. rexreusng
57. exsnrex
58. ralsn
59. rexsn
60. elunsn
61. elpwunsn
62. eqoreldif
63. eltpg
64. eldiftp
65. eltpi
66. eltp
67. el7g
68. dftp2
69. nfpr
70. ifpr
71. ralprgf
72. rexprgf
73. ralprg
74. rexprg
75. raltpg
76. rextpg
77. ralpr
78. rexpr
79. reuprg0
80. reuprg
81. reurexprg
82. raltp
83. rextp
84. nfsn
85. csbsng
86. csbprg
87. elinsn
88. disjsn
89. disjsn2
90. disjpr2
91. disjprsn
92. disjtpsn
93. disjtp2
94. snprc
95. snnzb
96. rmosn
97. r19.12sn
98. rabsn
99. rabsnifsb
100. rabsnif
101. rabrsn
102. euabsn2
103. euabsn
104. reusn
105. absneu
106. rabsneu
107. eusn
108. rabsnt
109. prcom
110. preq1
111. preq2
112. preq12
113. preq1i
114. preq2i
115. preq12i
116. preq1d
117. preq2d
118. preq12d
119. tpeq1
120. tpeq2
121. tpeq3
122. tpeq1d
123. tpeq2d
124. tpeq3d
125. tpeq123d
126. tprot
127. tpcoma
128. tpcomb
129. tpass
130. qdass
131. qdassr
132. tpidm12
133. tpidm13
134. tpidm23
135. tpidm
136. tppreq3
137. prid1g
138. prid2g
139. prid1
140. prid2
141. ifpprsnss
142. prprc1
143. prprc2
144. prprc
145. tpid1
146. tpid1g
147. tpid2
148. tpid2g
149. tpid3g
150. tpid3
151. snnzg
152. snn0d
153. snnz
154. prnz
155. prnzg
156. tpnz
157. tpnzd
158. raltpd
159. snssb
160. snssg
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. 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. 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. 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. iunidOLD
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. iindif1
85. 2iunin
86. iindif2
87. iinin2
88. iinin1
89. iinvdif
90. elriin
91. riin0
92. riinn0
93. riinrab
94. symdif0
95. symdifv
96. symdifid
97. iinxsng
98. iinxprg
99. iunxsng
100. iunxsn
101. iunxsngf
102. iunun
103. iunxun
104. iunxdif3
105. iunxprg
106. iunxiun
107. iinuni
108. iununi
109. sspwuni
110. pwssb
111. elpwpw
112. pwpwab
113. pwpwssunieq
114. elpwuni
115. iinpw
116. iunpwss
117. intss2
118. 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