Metamath Proof Explorer


Table of Contents - 2.1. ZF Set Theory - start with the Axiom of Extensionality

  1. Introduce the Axiom of Extensionality
    1. ax-ext
    2. axexte
    3. axextg
    4. axextb
    5. axextmo
    6. nulmo
  2. Classes
    1. Class abstractions
    2. Class equality
    3. Class membership
    4. Elementary properties of class abstractions
  3. Class form not-free predicate
    1. wnfc
    2. nfcjust
    3. df-nfc
    4. nfci
    5. nfcii
    6. nfcr
    7. nfcriv
    8. nfcd
    9. nfcrd
    10. nfcrii
    11. nfcri
    12. nfceqdf
    13. nfceqi
    14. nfceqiOLD
    15. nfcxfr
    16. nfcxfrd
    17. nfcv
    18. nfcvd
    19. nfab1
    20. nfnfc1
    21. clelsb3fw
    22. clelsb3f
    23. clelsb3fOLD
    24. nfab
    25. nfabg
    26. nfaba1
    27. nfaba1g
    28. nfeqd
    29. nfeld
    30. nfnfc
    31. nfeq
    32. nfel
    33. nfeq1
    34. nfel1
    35. nfeq2
    36. nfel2
    37. drnfc1
    38. drnfc1OLD
    39. drnfc2
    40. nfabdw
    41. nfabd
    42. nfabd2
    43. nfabd2OLD
    44. nfabdOLD
    45. dvelimdc
    46. dvelimc
    47. nfcvf
    48. nfcvf2
    49. nfcvfOLD
    50. cleqf
    51. cleqfOLD
    52. abid2f
    53. abeq2f
    54. abeq2fOLD
    55. sbabel
  4. Negated equality and membership
    1. Negated equality
    2. Negated membership
  5. Restricted quantification
    1. wral
    2. wrex
    3. wreu
    4. wrmo
    5. crab
    6. df-ral
    7. df-rex
    8. df-reu
    9. df-rmo
    10. df-rab
    11. rgen
    12. ralel
    13. rgenw
    14. rgen2w
    15. mprg
    16. mprgbir
    17. alral
    18. raln
    19. ral2imi
    20. ralimi2
    21. ralimia
    22. ralimiaa
    23. ralimi
    24. 2ralimi
    25. ralim
    26. ralbii2
    27. ralbiia
    28. ralbii
    29. 2ralbii
    30. ralbi
    31. ralanid
    32. ralanidOLD
    33. r19.26
    34. r19.26-2
    35. r19.26-3
    36. r19.26m
    37. ralbiim
    38. r19.21v
    39. ralimdv2
    40. ralimdva
    41. ralimdv
    42. ralimdvva
    43. hbralrimi
    44. ralrimiv
    45. ralrimiva
    46. ralrimivw
    47. r19.27v
    48. r19.27vOLD
    49. r19.28v
    50. r19.28vOLD
    51. ralrimdv
    52. ralrimdva
    53. ralrimivv
    54. ralrimivva
    55. ralrimivvva
    56. ralrimdvv
    57. ralrimdvva
    58. ralbidv2
    59. ralbidva
    60. ralbidv
    61. 2ralbidva
    62. 2ralbidv
    63. r2allem
    64. r2al
    65. r3al
    66. rgen2
    67. rgen3
    68. rsp
    69. rspa
    70. rspec
    71. r19.21bi
    72. r19.21biOLD
    73. r19.21be
    74. rspec2
    75. rspec3
    76. rsp2
    77. r19.21t
    78. r19.21
    79. ralrimi
    80. ralimdaa
    81. ralrimd
    82. nfra1
    83. hbra1
    84. hbral
    85. r2alf
    86. nfraldw
    87. nfrald
    88. nfralw
    89. nfral
    90. nfra2w
    91. nfra2
    92. rgen2a
    93. ralbida
    94. ralbid
    95. 2ralbida
    96. ralbiOLD
    97. raleqbii
    98. ralcom4
    99. ralnex
    100. dfral2
    101. rexnal
    102. dfrex2
    103. rexex
    104. rexim
    105. reximia
    106. reximi
    107. reximi2
    108. rexbii2
    109. rexbiia
    110. rexbii
    111. 2rexbii
    112. rexcom4
    113. 2ex2rexrot
    114. rexcom4a
    115. rexanid
    116. rexanidOLD
    117. r19.29
    118. r19.29r
    119. r19.29rOLD
    120. r19.29imd
    121. rexnal2
    122. rexnal3
    123. ralnex2
    124. ralnex2OLD
    125. ralnex3
    126. ralnex3OLD
    127. ralinexa
    128. rexanali
    129. nrexralim
    130. risset
    131. nelb
    132. nrex
    133. nrexdv
    134. reximdv2
    135. reximdvai
    136. reximdv
    137. reximdva
    138. reximddv
    139. reximssdv
    140. reximdvva
    141. reximddv2
    142. r19.23v
    143. rexlimiv
    144. rexlimiva
    145. rexlimivw
    146. rexlimdv
    147. rexlimdva
    148. rexlimdvaa
    149. rexlimdv3a
    150. rexlimdva2
    151. r19.29an
    152. r19.29a
    153. rexlimdvw
    154. rexlimddv
    155. rexlimivv
    156. rexlimdvv
    157. rexlimdvva
    158. rexbidv2
    159. rexbidva
    160. rexbidv
    161. 2rexbiia
    162. 2rexbidva
    163. 2rexbidv
    164. rexralbidv
    165. r2exlem
    166. r2ex
    167. rspe
    168. rsp2e
    169. nfre1
    170. nfrexd
    171. nfrexdg
    172. nfrex
    173. nfrexg
    174. reximdai
    175. reximd2a
    176. r19.23t
    177. r19.23
    178. rexlimi
    179. rexlimd2
    180. rexlimd
    181. rexbida
    182. rexbidvaALT
    183. rexbid
    184. rexbidvALT
    185. ralrexbid
    186. ralrexbidOLD
    187. r19.12
    188. r2exf
    189. rexeqbii
    190. r19.12OLD
    191. reuanid
    192. rmoanid
    193. r19.29af2
    194. r19.29af
    195. r19.29anOLD
    196. r19.29aOLD
    197. 2r19.29
    198. r19.29d2r
    199. r19.29vva
    200. r19.29vvaOLD
    201. r19.30
    202. r19.30OLD
    203. r19.32v
    204. r19.35
    205. r19.36v
    206. r19.37
    207. r19.37v
    208. r19.37vOLD
    209. r19.40
    210. r19.41v
    211. r19.41
    212. r19.41vv
    213. r19.42v
    214. r19.43
    215. r19.44v
    216. r19.45v
    217. ralcom
    218. rexcom
    219. rexcomOLD
    220. ralcomf
    221. rexcomf
    222. ralcom13
    223. rexcom13
    224. ralrot3
    225. rexrot4
    226. ralcom2w
    227. ralcom2
    228. ralcom3
    229. reeanlem
    230. reean
    231. reeanv
    232. 3reeanv
    233. 2ralor
    234. nfreu1
    235. nfrmo1
    236. nfreud
    237. nfrmod
    238. nfreuw
    239. nfrmow
    240. nfreu
    241. nfrmo
    242. rabid
    243. rabrab
    244. rabidim1
    245. rabid2
    246. rabid2f
    247. rabbi
    248. nfrab1
    249. nfrabw
    250. nfrab
    251. reubida
    252. reubidva
    253. reubidv
    254. reubiia
    255. reubii
    256. rmobida
    257. rmobidva
    258. rmobidv
    259. rmobiia
    260. rmobii
    261. raleqf
    262. rexeqf
    263. reueq1f
    264. rmoeq1f
    265. raleqbidv
    266. rexeqbidv
    267. raleqbi1dv
    268. rexeqbi1dv
    269. raleq
    270. rexeq
    271. reueq1
    272. rmoeq1
    273. raleqOLD
    274. rexeqOLD
    275. reueq1OLD
    276. rmoeq1OLD
    277. raleqi
    278. rexeqi
    279. raleqdv
    280. rexeqdv
    281. raleqbi1dvOLD
    282. rexeqbi1dvOLD
    283. reueqd
    284. rmoeqd
    285. raleqbid
    286. rexeqbid
    287. raleqbidvOLD
    288. rexeqbidvOLD
    289. raleqbidva
    290. rexeqbidva
    291. raleleq
    292. raleleqALT
    293. mormo
    294. reu5
    295. reurex
    296. 2reu2rex
    297. reurmo
    298. rmo5
    299. nrexrmo
    300. reueubd
    301. cbvralfw
    302. cbvrexfw
    303. cbvralf
    304. cbvrexf
    305. cbvralw
    306. cbvrexw
    307. cbvreuw
    308. cbvrmow
    309. cbvral
    310. cbvrex
    311. cbvreu
    312. cbvrmo
    313. cbvralvw
    314. cbvrexvw
    315. cbvreuvw
    316. cbvralv
    317. cbvrexv
    318. cbvreuv
    319. cbvrmov
    320. cbvraldva2
    321. cbvrexdva2
    322. cbvrexdva2OLD
    323. cbvraldva
    324. cbvrexdva
    325. cbvral2vw
    326. cbvrex2vw
    327. cbvral3vw
    328. cbvral2v
    329. cbvrex2v
    330. cbvral3v
    331. cbvralsvw
    332. cbvrexsvw
    333. cbvralsv
    334. cbvrexsv
    335. sbralie
    336. rabbiia
    337. rabbii
    338. rabbida
    339. rabbid
    340. rabbidva2
    341. rabbia2
    342. rabbidva
    343. rabbidvaOLD
    344. rabbidv
    345. rabeqf
    346. rabeqi
    347. rabeq
    348. rabeqdv
    349. rabeqbidv
    350. rabeqbidva
    351. rabeq2i
    352. rabswap
    353. cbvrabw
    354. cbvrab
    355. cbvrabv
    356. cbvrabvOLD
    357. rabrabi
  6. The universal class
    1. cvv
    2. vjust
    3. df-v
    4. vex
    5. vexOLD
    6. elv
    7. elvd
    8. el2v
    9. eqv
    10. eqvf
    11. abv
    12. elisset
    13. isset
    14. issetf
    15. isseti
    16. issetiOLD
    17. issetri
    18. eqvisset
    19. elex
    20. elexi
    21. elexd
    22. elissetOLD
    23. elex2
    24. elex22
    25. prcnel
    26. ralv
    27. rexv
    28. reuv
    29. rmov
    30. rabab
    31. rexcom4b
    32. ralcom4OLD
    33. rexcom4OLD
    34. ceqsalt
    35. ceqsralt
    36. ceqsalg
    37. ceqsalgALT
    38. ceqsal
    39. ceqsalv
    40. ceqsralv
    41. gencl
    42. 2gencl
    43. 3gencl
    44. cgsexg
    45. cgsex2g
    46. cgsex4g
    47. ceqsex
    48. ceqsexv
    49. ceqsexv2d
    50. ceqsex2
    51. ceqsex2v
    52. ceqsex3v
    53. ceqsex4v
    54. ceqsex6v
    55. ceqsex8v
    56. gencbvex
    57. gencbvex2
    58. gencbval
    59. sbhypf
    60. vtoclgft
    61. vtoclgftOLD
    62. vtocldf
    63. vtocld
    64. vtocl2d
    65. vtoclf
    66. vtocl
    67. vtoclALT
    68. vtocl2
    69. vtocl2OLD
    70. vtocl3
    71. vtoclb
    72. vtoclgf
    73. vtoclg1f
    74. vtoclg
    75. vtoclbg
    76. vtocl2gf
    77. vtocl3gf
    78. vtocl2g
    79. vtoclgaf
    80. vtoclga
    81. vtocl2ga
    82. vtocl2gaf
    83. vtocl3gaf
    84. vtocl3ga
    85. vtocl4g
    86. vtocl4ga
    87. vtocleg
    88. vtoclegft
    89. vtoclef
    90. vtocle
    91. vtoclri
    92. spcimgft
    93. spcgft
    94. spcimgf
    95. spcimegf
    96. spcgf
    97. spcegf
    98. spcimdv
    99. spcdv
    100. spcimedv
    101. spcgv
    102. spcgvOLD
    103. spcegv
    104. spcegvOLD
    105. spcedv
    106. spc2egv
    107. spc2gv
    108. spc2ed
    109. spc2d
    110. spc3egv
    111. spc3gv
    112. spcv
    113. spcev
    114. spc2ev
    115. rspct
    116. rspcdf
    117. rspc
    118. rspce
    119. rspcimdv
    120. rspcimedv
    121. rspcdv
    122. rspcedv
    123. rspcebdv
    124. rspcv
    125. rspcvOLD
    126. rspccv
    127. rspcva
    128. rspccva
    129. rspcev
    130. rspcevOLD
    131. rspcdva
    132. rspcedvd
    133. rspcime
    134. rspceaimv
    135. rspcedeq1vd
    136. rspcedeq2vd
    137. rspc2
    138. rspc2gv
    139. rspc2v
    140. rspc2va
    141. rspc2ev
    142. rspc3v
    143. rspc3ev
    144. rspceeqv
    145. ralxpxfr2d
    146. rexraleqim
    147. eqvincg
    148. eqvinc
    149. eqvincf
    150. alexeqg
    151. ceqex
    152. ceqsexg
    153. ceqsexgv
    154. ceqsexgvOLD
    155. ceqsrexv
    156. ceqsrexbv
    157. ceqsrex2v
    158. clel2g
    159. clel2
    160. clel3g
    161. clel3
    162. clel4
    163. clel5
    164. clel5OLD
    165. pm13.183
    166. pm13.183OLD
    167. rr19.3v
    168. rr19.28v
    169. elabgt
    170. elabgf
    171. elabf
    172. elabg
    173. elab
    174. elab2g
    175. elabd
    176. elab2
    177. elab4g
    178. elab3gf
    179. elab3g
    180. elab3
    181. elrabi
    182. elrabf
    183. rabtru
    184. rabeqc
    185. elrab3t
    186. elrab
    187. elrab3
    188. elrabd
    189. elrab2
    190. ralab
    191. ralrab
    192. rexab
    193. rexrab
    194. ralab2
    195. ralab2OLD
    196. ralrab2
    197. rexab2
    198. rexab2OLD
    199. rexrab2
    200. abidnf
    201. dedhb
    202. nelrdva
    203. eqeu
    204. moeq
    205. eueq
    206. eueqi
    207. eueq2
    208. eueq3
    209. moeq3
    210. mosub
    211. mo2icl
    212. mob2
    213. moi2
    214. mob
    215. moi
    216. morex
    217. euxfr2w
    218. euxfrw
    219. euxfr2
    220. euxfr
    221. euind
    222. reu2
    223. reu6
    224. reu3
    225. reu6i
    226. eqreu
    227. rmo4
    228. reu4
    229. reu7
    230. reu8
    231. rmo3f
    232. rmo4f
    233. reu2eqd
    234. reueq
    235. rmoeq
    236. rmoan
    237. rmoim
    238. rmoimia
    239. rmoimi
    240. rmoimi2
    241. 2reu5a
    242. reuimrmo
    243. 2reuswap
    244. 2reuswap2
    245. reuxfrd
    246. reuxfr
    247. reuxfr1d
    248. reuxfr1ds
    249. reuxfr1
    250. reuind
    251. 2rmorex
    252. 2reu5lem1
    253. 2reu5lem2
    254. 2reu5lem3
    255. 2reu5
    256. 2reurex
    257. 2reurmo
    258. 2rmoswap
    259. 2rexreu
  7. 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
  8. Russell's Paradox
    1. rru
    2. ru
  9. 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. sbc6g
    31. sbc6
    32. sbc7
    33. cbvsbcw
    34. cbvsbcvw
    35. cbvsbc
    36. cbvsbcv
    37. sbciegft
    38. sbciegf
    39. sbcieg
    40. sbcie2g
    41. sbcie
    42. sbciedf
    43. sbcied
    44. sbcied2
    45. elrabsf
    46. eqsbc3
    47. eqsbc3OLD
    48. sbcng
    49. sbcimg
    50. sbcan
    51. sbcor
    52. sbcbig
    53. sbcn1
    54. sbcim1
    55. sbcbid
    56. sbcbidv
    57. sbcbidvOLD
    58. sbcbii
    59. sbcbi1
    60. sbcbi2
    61. sbcbi2OLD
    62. sbcal
    63. sbcex2
    64. sbceqal
    65. sbeqalb
    66. eqsbc3r
    67. sbc3an
    68. sbcel1v
    69. sbcel1vOLD
    70. sbcel2gv
    71. sbcel21v
    72. sbcimdv
    73. sbctt
    74. sbcgf
    75. sbc19.21g
    76. sbcg
    77. sbcgfi
    78. sbc2iegf
    79. sbc2ie
    80. sbc2iedv
    81. sbc3ie
    82. sbccomlem
    83. sbccom
    84. sbcralt
    85. sbcrext
    86. sbcralg
    87. sbcrex
    88. sbcreu
    89. reu8nf
    90. sbcabel
    91. rspsbc
    92. rspsbca
    93. rspesbca
    94. spesbc
    95. spesbcd
    96. sbcth2
    97. ra4v
    98. ra4
    99. rmo2
    100. rmo2i
    101. rmo3
    102. rmo3OLD
    103. rmob
    104. rmoi
    105. rmob2
    106. rmoi2
    107. rmoanim
    108. rmoanimALT
    109. reuan
    110. 2reu1
    111. 2reu2
  10. 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. vtocl2dOLD
    50. rspc2vd
  11. 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
  12. Subclasses and subsets
    1. df-ss
    2. dfss
    3. df-pss
    4. dfss2
    5. dfss3
    6. dfss6
    7. dfss2f
    8. dfss3f
    9. nfss
    10. ssel
    11. ssel2
    12. sseli
    13. sselii
    14. sseldi
    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. eqsstri
    51. eqsstrri
    52. sseqtri
    53. sseqtrri
    54. eqsstrd
    55. eqsstrrd
    56. sseqtrd
    57. sseqtrrd
    58. 3sstr3i
    59. 3sstr4i
    60. 3sstr3g
    61. 3sstr4g
    62. 3sstr3d
    63. 3sstr4d
    64. eqsstrid
    65. eqsstrrid
    66. sseqtrdi
    67. sseqtrrdi
    68. sseqtrid
    69. sseqtrrid
    70. eqsstrdi
    71. eqsstrrdi
    72. eqimss
    73. eqimss2
    74. eqimssi
    75. eqimss2i
    76. nssne1
    77. nssne2
    78. nss
    79. nelss
    80. ssrexf
    81. ssrmof
    82. ssralv
    83. ssrexv
    84. ss2ralv
    85. ss2rexv
    86. ralss
    87. rexss
    88. ss2ab
    89. abss
    90. ssab
    91. ssabral
    92. ss2abi
    93. ss2abdv
    94. abssdv
    95. abssi
    96. ss2rab
    97. rabss
    98. ssrab
    99. ssrabdv
    100. rabssdv
    101. ss2rabdv
    102. ss2rabi
    103. rabss2
    104. ssab2
    105. ssrab2
    106. ssrab3
    107. rabssrabd
    108. ssrabeq
    109. rabssab
    110. uniiunlem
    111. dfpss2
    112. dfpss3
    113. psseq1
    114. psseq2
    115. psseq1i
    116. psseq2i
    117. psseq12i
    118. psseq1d
    119. psseq2d
    120. psseq12d
    121. pssss
    122. pssne
    123. pssssd
    124. pssned
    125. sspss
    126. pssirr
    127. pssn2lp
    128. sspsstri
    129. ssnpss
    130. psstr
    131. sspsstr
    132. psssstr
    133. psstrd
    134. sspsstrd
    135. psssstrd
    136. npss
    137. ssnelpss
    138. ssnelpssd
    139. ssexnelpss
  13. 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
  14. The empty set
    1. c0
    2. df-nul
    3. dfnul2
    4. dfnul2OLD
    5. dfnul3
    6. noel
    7. noelOLD
    8. nel02
    9. n0i
    10. ne0i
    11. ne0d
    12. n0ii
    13. ne0ii
    14. vn0
    15. eq0f
    16. neq0f
    17. n0f
    18. eq0
    19. neq0
    20. n0
    21. nel0
    22. reximdva0
    23. rspn0
    24. n0rex
    25. ssn0rex
    26. n0moeu
    27. rex0
    28. reu0
    29. rmo0
    30. 0el
    31. n0el
    32. eqeuel
    33. ssdif0
    34. difn0
    35. pssdifn0
    36. pssdif
    37. ndisj
    38. difin0ss
    39. inssdif0
    40. difid
    41. difidALT
    42. dif0
    43. ab0
    44. dfnf5
    45. ab0orv
    46. abn0
    47. rab0
    48. rabeq0
    49. rabn0
    50. rabxm
    51. rabnc
    52. elneldisj
    53. elnelun
    54. un0
    55. in0
    56. 0un
    57. 0in
    58. inv1
    59. unv
    60. 0ss
    61. ss0b
    62. ss0
    63. sseq0
    64. ssn0
    65. 0dif
    66. abf
    67. eq0rdv
    68. csbprc
    69. csb0
    70. sbcel12
    71. sbceqg
    72. sbceqi
    73. sbcnel12g
    74. sbcne12
    75. sbcel1g
    76. sbceq1g
    77. sbcel2
    78. sbceq2g
    79. csbcom
    80. sbcnestgfw
    81. csbnestgfw
    82. sbcnestgw
    83. csbnestgw
    84. sbcco3gw
    85. sbcnestgf
    86. csbnestgf
    87. sbcnestg
    88. csbnestg
    89. sbcco3g
    90. csbco3g
    91. csbnest1g
    92. csbidm
    93. csbvarg
    94. csbvargi
    95. sbccsb
    96. sbccsb2
    97. rspcsbela
    98. sbnfc2
    99. csbab
    100. csbun
    101. csbin
    102. 2nreu
    103. un00
    104. vss
    105. 0pss
    106. npss0
    107. pssv
    108. disj
    109. disjr
    110. disj1
    111. reldisj
    112. disj3
    113. disjne
    114. disjeq0
    115. disjel
    116. disj2
    117. disj4
    118. ssdisj
    119. disjpss
    120. undisj1
    121. undisj2
    122. ssindif0
    123. inelcm
    124. minel
    125. undif4
    126. disjssun
    127. vdif0
    128. difrab0eq
    129. pssnel
    130. disjdif
    131. difin0
    132. unvdif
    133. undif1
    134. undif2
    135. undifabs
    136. inundif
    137. disjdif2
    138. difun2
    139. undif
    140. ssdifin0
    141. ssdifeq0
    142. ssundif
    143. difcom
    144. pssdifcom1
    145. pssdifcom2
    146. difdifdir
    147. uneqdifeq
    148. raldifeq
    149. r19.2z
    150. r19.2zb
    151. r19.3rz
    152. r19.28z
    153. r19.3rzv
    154. r19.9rzv
    155. r19.28zv
    156. r19.37zv
    157. r19.45zv
    158. r19.44zv
    159. r19.27z
    160. r19.27zv
    161. r19.36zv
    162. rzal
    163. rexn0
    164. ralidm
    165. ral0
    166. ralf0
    167. ralnralall
    168. falseral0
    169. raaan
    170. raaanv
    171. sbss
    172. sbcssg
    173. raaan2
    174. 2reu4lem
    175. 2reu4
  15. 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. ifeq12
    19. ifeq1d
    20. ifeq2d
    21. ifeq12d
    22. ifbi
    23. ifbid
    24. ifbieq1d
    25. ifbieq2i
    26. ifbieq2d
    27. ifbieq12i
    28. ifbieq12d
    29. nfifd
    30. nfif
    31. ifeq1da
    32. ifeq2da
    33. ifeq12da
    34. ifbieq12d2
    35. ifclda
    36. ifeqda
    37. elimif
    38. ifbothda
    39. ifboth
    40. ifid
    41. eqif
    42. ifval
    43. elif
    44. ifel
    45. ifcl
    46. ifcld
    47. ifcli
    48. ifexg
    49. ifex
    50. ifeqor
    51. ifnot
    52. ifan
    53. ifor
    54. 2if2
    55. ifcomnan
    56. csbif
  16. 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
  17. Power classes
    1. cpw
    2. pwjust
    3. df-pw
    4. pweq
    5. pweqi
    6. pweqd
    7. elpwg
    8. elpw
    9. velpw
    10. elpwOLD
    11. elpwgOLD
    12. elpwd
    13. elpwi
    14. elpwb
    15. elpwid
    16. elelpwi
    17. nfpw
    18. pwidg
    19. pwidb
    20. pwid
    21. pwss
  18. 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. elpr2
    27. nelpr2
    28. nelpr1
    29. nelpri
    30. prneli
    31. nelprd
    32. eldifpr
    33. rexdifpr
    34. snidg
    35. snidb
    36. snid
    37. vsnid
    38. elsn2g
    39. elsn2
    40. nelsn
    41. rabeqsn
    42. rabsssn
    43. ralsnsg
    44. rexsns
    45. ralsngOLD
    46. rexsngOLD
    47. rexsngf
    48. ralsngf
    49. reusngf
    50. ralsng
    51. rexsng
    52. reusng
    53. 2ralsng
    54. rexreusng
    55. exsnrex
    56. ralsn
    57. rexsn
    58. elpwunsn
    59. eqoreldif
    60. eltpg
    61. eldiftp
    62. eltpi
    63. eltp
    64. dftp2
    65. nfpr
    66. ifpr
    67. ralprgf
    68. rexprgf
    69. ralprg
    70. rexprg
    71. raltpg
    72. rextpg
    73. ralpr
    74. rexpr
    75. reuprg0
    76. reuprg
    77. reurexprg
    78. raltp
    79. rextp
    80. nfsn
    81. csbsng
    82. csbprg
    83. elinsn
    84. disjsn
    85. disjsn2
    86. disjpr2
    87. disjprsn
    88. disjtpsn
    89. disjtp2
    90. snprc
    91. snnzb
    92. rmosn
    93. r19.12sn
    94. rabsn
    95. rabsnifsb
    96. rabsnif
    97. rabrsn
    98. euabsn2
    99. euabsn
    100. reusn
    101. absneu
    102. rabsneu
    103. eusn
    104. rabsnt
    105. prcom
    106. preq1
    107. preq2
    108. preq12
    109. preq1i
    110. preq2i
    111. preq12i
    112. preq1d
    113. preq2d
    114. preq12d
    115. tpeq1
    116. tpeq2
    117. tpeq3
    118. tpeq1d
    119. tpeq2d
    120. tpeq3d
    121. tpeq123d
    122. tprot
    123. tpcoma
    124. tpcomb
    125. tpass
    126. qdass
    127. qdassr
    128. tpidm12
    129. tpidm13
    130. tpidm23
    131. tpidm
    132. tppreq3
    133. prid1g
    134. prid2g
    135. prid1
    136. prid2
    137. ifpprsnss
    138. prprc1
    139. prprc2
    140. prprc
    141. tpid1
    142. tpid1g
    143. tpid2
    144. tpid2g
    145. tpid3g
    146. tpid3
    147. snnzg
    148. snnz
    149. prnz
    150. prnzg
    151. tpnz
    152. tpnzd
    153. raltpd
    154. snssg
    155. snss
    156. eldifsn
    157. ssdifsn
    158. elpwdifsn
    159. eldifsni
    160. eldifsnneq
    161. eldifsnneqOLD
    162. neldifsn
    163. neldifsnd
    164. rexdifsn
    165. raldifsni
    166. raldifsnb
    167. eldifvsn
    168. difsn
    169. difprsnss
    170. difprsn1
    171. difprsn2
    172. diftpsn3
    173. difpr
    174. tpprceq3
    175. tppreqb
    176. difsnb
    177. difsnpss
    178. snssi
    179. snssd
    180. difsnid
    181. eldifeldifsn
    182. pw0
    183. pwpw0
    184. snsspr1
    185. snsspr2
    186. snsstp1
    187. snsstp2
    188. snsstp3
    189. prssg
    190. prss
    191. prssi
    192. prssd
    193. prsspwg
    194. ssprss
    195. ssprsseq
    196. sssn
    197. ssunsn2
    198. ssunsn
    199. eqsn
    200. issn
    201. n0snor2el
    202. ssunpr
    203. sspr
    204. sstp
    205. tpss
    206. tpssi
    207. sneqrg
    208. sneqr
    209. snsssn
    210. mosneq
    211. sneqbg
    212. snsspw
    213. prsspw
    214. preq1b
    215. preq2b
    216. preqr1
    217. preqr2
    218. preq12b
    219. opthpr
    220. preqr1g
    221. preq12bg
    222. prneimg
    223. prnebg
    224. pr1eqbg
    225. pr1nebg
    226. preqsnd
    227. prnesn
    228. prneprprc
    229. preqsn
    230. preq12nebg
    231. prel12g
    232. opthprneg
    233. elpreqprlem
    234. elpreqpr
    235. elpreqprb
    236. elpr2elpr
    237. dfopif
    238. dfopg
    239. dfop
    240. opeq1
    241. opeq2
    242. opeq12
    243. opeq1i
    244. opeq2i
    245. opeq12i
    246. opeq1d
    247. opeq2d
    248. opeq12d
    249. oteq1
    250. oteq2
    251. oteq3
    252. oteq1d
    253. oteq2d
    254. oteq3d
    255. oteq123d
    256. nfop
    257. nfopd
    258. csbopg
    259. opidg
    260. opid
    261. ralunsn
    262. 2ralunsn
    263. opprc
    264. opprc1
    265. opprc2
    266. oprcl
    267. pwsn
    268. pwsnALT
    269. pwpr
    270. pwtp
    271. pwpwpw0
    272. pwv
    273. prproe
    274. 3elpr2eq
  19. The union of a class
    1. cuni
    2. df-uni
    3. dfuni2
    4. eluni
    5. eluni2
    6. elunii
    7. nfunid
    8. nfuni
    9. unieq
    10. unieqi
    11. unieqd
    12. eluniab
    13. elunirab
    14. unipr
    15. uniprg
    16. unisng
    17. unisn
    18. unisn3
    19. dfnfc2
    20. uniun
    21. uniin
    22. uniss
    23. ssuni
    24. unissi
    25. unissd
    26. uni0b
    27. uni0c
    28. uni0
    29. csbuni
    30. elssuni
    31. unissel
    32. unissb
    33. uniss2
    34. unidif
    35. ssunieq
    36. unimax
    37. pwuni
  20. 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. elintab
    13. elintrab
    14. elintrabg
    15. int0
    16. intss1
    17. ssint
    18. ssintab
    19. ssintub
    20. ssmin
    21. intmin
    22. intss
    23. intssuni
    24. ssintrab
    25. unissint
    26. intssuni2
    27. intminss
    28. intmin2
    29. intmin3
    30. intmin4
    31. intab
    32. int0el
    33. intun
    34. intpr
    35. intprg
    36. intsng
    37. intsn
    38. uniintsn
    39. uniintab
    40. intunsn
    41. rint0
    42. elrint
    43. elrint2
  21. 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. iunss
    52. ssiun
    53. ssiun2
    54. ssiun2s
    55. iunss2
    56. iunssd
    57. iunab
    58. iunrab
    59. iunxdif2
    60. ssiinf
    61. ssiin
    62. iinss
    63. iinss2
    64. uniiun
    65. intiin
    66. iunid
    67. iun0
    68. 0iun
    69. 0iin
    70. viin
    71. iunn0
    72. iinab
    73. iinrab
    74. iinrab2
    75. iunin2
    76. iunin1
    77. iinun2
    78. iundif2
    79. iindif1
    80. 2iunin
    81. iindif2
    82. iinin2
    83. iinin1
    84. iinvdif
    85. elriin
    86. riin0
    87. riinn0
    88. riinrab
    89. symdif0
    90. symdifv
    91. symdifid
    92. iinxsng
    93. iinxprg
    94. iunxsng
    95. iunxsn
    96. iunxsngf
    97. iunun
    98. iunxun
    99. iunxdif3
    100. iunxprg
    101. iunxiun
    102. iinuni
    103. iununi
    104. sspwuni
    105. pwssb
    106. elpwpw
    107. pwpwab
    108. pwpwssunieq
    109. elpwuni
    110. iinpw
    111. iunpwss
    112. rintn0
  22. 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
  23. 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
  24. Ordered-pair class abstractions (class builders)
    1. copab
    2. df-opab
    3. opabss
    4. opabbid
    5. opabbidv
    6. opabbii
    7. nfopab
    8. nfopab1
    9. nfopab2
    10. cbvopab
    11. cbvopabv
    12. cbvopab1
    13. cbvopab1g
    14. cbvopab2
    15. cbvopab1s
    16. cbvopab1v
    17. cbvopab2v
    18. unopab
  25. Functions in maps-to notation
    1. cmpt
    2. df-mpt
    3. mpteq12df
    4. mpteq12f
    5. mpteq12dva
    6. mpteq12dv
    7. mpteq12dvOLD
    8. mpteq12
    9. mpteq1
    10. mpteq1d
    11. mpteq1i
    12. mpteq2ia
    13. mpteq2i
    14. mpteq12i
    15. mpteq2da
    16. mpteq2dva
    17. mpteq2dv
    18. nfmpt
    19. nfmpt1
    20. cbvmptf
    21. cbvmptfg
    22. cbvmpt
    23. cbvmptg
    24. cbvmptv
    25. cbvmptvg
    26. mptv
  26. Transitive classes
    1. wtr
    2. df-tr
    3. dftr2
    4. dftr5
    5. dftr3
    6. dftr4
    7. treq
    8. trel
    9. trel3
    10. trss
    11. trin
    12. tr0
    13. trv
    14. triun
    15. truni
    16. triin
    17. trint
    18. trintss