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. ceqsexv2dOLD
52. ceqsex2
53. ceqsex2v
54. ceqsex3v
55. ceqsex4v
56. ceqsex6v
57. ceqsex8v
58. gencbvex
59. gencbvex2
60. gencbval
61. sbhypf
62. spcimgft
63. spcimgfi1
64. spcimgfi1OLD
65. spcgft
66. spcimgf
67. spcimegf
68. vtoclgft
69. vtocleg
70. vtoclg
71. vtocle
72. vtoclbg
73. vtocl
74. vtoclOLD
75. vtocldf
76. vtocld
77. vtocl2d
78. vtoclef
79. vtoclf
80. vtocl2
81. vtocl3
82. vtoclb
83. vtoclgf
84. vtoclg1f
85. vtocl2gf
86. vtocl3gf
87. vtocl2g
88. vtocl3g
89. vtoclgaf
90. vtoclga
91. vtocl2ga
92. vtocl2gaf
93. vtocl3gaf
94. vtocl3ga
95. vtocl4g
96. vtocl4ga
97. vtoclegft
98. vtoclri
99. spcgf
100. spcegf
101. spcimdv
102. spcdv
103. spcimedv
104. spcgv
105. spcegv
106. spcedv
107. spc2egv
108. spc2gv
109. spc2ed
110. spc2d
111. spc3egv
112. spc3gv
113. spcv
114. spcev
115. spc2ev
116. rspct
117. rspcdf
118. rspc
119. rspce
120. rspcimdv
121. rspcimedv
122. rspcdv
123. rspcedv
124. rspcebdv
125. rspcdv2
126. rspcv
127. rspccv
128. rspcva
129. rspccva
130. rspcev
131. rspcdva
132. rspcedvd
133. rspcedvdw
134. rspceb2dv
135. rspcime
136. rspceaimv
137. rspcedeq1vd
138. rspcedeq2vd
139. rspc2
140. rspc2gv
141. rspc2v
142. rspc2va
143. rspc2ev
144. 2rspcedvdw
145. rspc2dv
146. rspc3v
147. rspc3ev
148. 3rspcedvdw
149. rspc3dv
150. rspc4v
151. rspc6v
152. rspc8v
153. rspceeqv
154. ralxpxfr2d
155. rexraleqim
156. eqvincg
157. eqvinc
158. eqvincf
159. alexeqg
160. ceqex
161. ceqsexg
162. ceqsexgv
163. ceqsrexv
164. ceqsrexbv
165. ceqsralbv
166. ceqsrex2v
167. clel2g
168. clel2
169. clel3g
170. clel3
171. clel4g
172. clel4
173. clel5
174. pm13.183
175. rr19.3v
176. rr19.28v
177. elab6g
178. elabd2
179. elabd3
180. elabgt
181. elabgtOLD
182. elabgf
183. elabf
184. elabg
185. elabgw
186. elab2gw
187. elab
188. elab2g
189. elabd
190. elab2
191. elab4g
192. elab3gf
193. elab3g
194. elab3
195. elrabi
196. elrabf
197. rabtru
198. elrab3t
199. elrab
200. elrab3
201. elrabd
202. elrab2
203. elrab2w
204. ralab
205. ralrab
206. rexab
207. rexrab
208. ralab2
209. ralrab2
210. rexab2
211. rexrab2
212. reurab
213. abidnf
214. dedhb
215. class2seteq
216. nelrdva
217. eqeu
218. moeq
219. eueq
220. eueqi
221. eueq2
222. eueq3
223. moeq3
224. mosub
225. mo2icl
226. mob2
227. moi2
228. mob
229. moi
230. morex
231. euxfr2w
232. euxfrw
233. euxfr2
234. euxfr
235. euind
236. reu2
237. reu6
238. reu3
239. reu6i
240. eqreu
241. rmo4
242. reu4
243. reu7
244. reu8
245. rmo3f
246. rmo4f
247. reu2eqd
248. reueq
249. rmoeq
250. rmoan
251. rmoim
252. rmoimia
253. rmoimi
254. rmoimi2
255. 2reu5a
256. reuimrmo
257. 2reuswap
258. 2reuswap2
259. reuxfrd
260. reuxfr
261. reuxfr1d
262. reuxfr1ds
263. reuxfr1
264. reuind
265. 2rmorex
266. 2reu5lem1
267. 2reu5lem2
268. 2reu5lem3
269. 2reu5
270. 2reurmo
271. 2reurex
272. 2rmoswap
273. 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. 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. rmob2
103. rmoi2
104. rmoanim
105. rmoanimALT
106. reuan
107. 2reu1
108. 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. 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. undif5
153. ssdifin0
154. ssdifeq0
155. ssundif
156. difcom
157. pssdifcom1
158. pssdifcom2
159. difdifdir
160. uneqdifeq
161. raldifeq
162. rzal
163. rzalALT
164. rexn0
165. ralf0
166. ral0
167. r19.2z
168. r19.2zb
169. r19.3rz
170. r19.28z
171. r19.3rzv
172. r19.3rzvOLD
173. r19.9rzv
174. r19.28zv
175. r19.37zv
176. r19.45zv
177. r19.44zv
178. r19.27z
179. r19.27zv
180. r19.36zv
181. ralnralall
182. falseral0
183. falseral0OLD
184. ralidmw
185. ralidm
186. raaan
187. raaanv
188. sbss
189. sbcssg
190. raaan2
191. 2reu4lem
192. 2reu4
193. 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. snssi
165. snssd
166. eldifsn
167. eldifsnd
168. ssdifsn
169. elpwdifsn
170. eldifsni
171. eldifsnneq
172. neldifsn
173. neldifsnd
174. rexdifsn
175. raldifsni
176. raldifsnb
177. eldifvsn
178. difsn
179. difprsnss
180. difprsn1
181. difprsn2
182. diftpsn3
183. difpr
184. tpprceq3
185. tppreqb
186. difsnb
187. difsnpss
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. uni0OLD
31. csbuni
32. elssuni
33. unissel
34. unissb
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. 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. 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. trun
13. trin
14. tr0
15. trv
16. triun
17. truni
18. triin
19. trint
20. trintss