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. nfcrALT
    8. nfcriv
    9. nfcd
    10. nfcrd
    11. nfcri
    12. nfcriOLD
    13. nfcrii
    14. nfcriiOLD
    15. nfcriOLDOLD
    16. nfceqdf
    17. nfceqi
    18. nfceqiOLD
    19. nfcxfr
    20. nfcxfrd
    21. nfcv
    22. nfcvd
    23. nfab1
    24. nfnfc1
    25. clelsb3fw
    26. clelsb3f
    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. drnfc2
    42. nfabdw
    43. nfabd
    44. nfabd2
    45. dvelimdc
    46. dvelimc
    47. nfcvf
    48. nfcvf2
    49. cleqf
    50. abid2f
    51. abeq2f
    52. 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. ralnex3
    125. ralinexa
    126. rexanali
    127. nrexralim
    128. risset
    129. nelb
    130. nrex
    131. nrexdv
    132. reximdv2
    133. reximdvai
    134. reximdv
    135. reximdva
    136. reximddv
    137. reximssdv
    138. reximdvva
    139. reximddv2
    140. r19.23v
    141. rexlimiv
    142. rexlimiva
    143. rexlimivw
    144. rexlimdv
    145. rexlimdva
    146. rexlimdvaa
    147. rexlimdv3a
    148. rexlimdva2
    149. r19.29an
    150. r19.29a
    151. rexlimdvw
    152. rexlimddv
    153. rexlimivv
    154. rexlimdvv
    155. rexlimdvva
    156. rexbidv2
    157. rexbidva
    158. rexbidv
    159. 2rexbiia
    160. 2rexbidva
    161. 2rexbidv
    162. rexralbidv
    163. r2exlem
    164. r2ex
    165. rspe
    166. rsp2e
    167. nfre1
    168. nfrexd
    169. nfrexdg
    170. nfrex
    171. nfrexg
    172. reximdai
    173. reximd2a
    174. r19.23t
    175. r19.23
    176. rexlimi
    177. rexlimd2
    178. rexlimd
    179. rexbida
    180. rexbidvaALT
    181. rexbid
    182. rexbidvALT
    183. ralrexbid
    184. ralrexbidOLD
    185. r19.12
    186. r2exf
    187. rexeqbii
    188. reuanid
    189. rmoanid
    190. r19.29af2
    191. r19.29af
    192. r19.29anOLD
    193. r19.29aOLD
    194. 2r19.29
    195. r19.29d2r
    196. r19.29vva
    197. r19.29vvaOLD
    198. r19.30
    199. r19.30OLD
    200. r19.32v
    201. r19.35
    202. r19.36v
    203. r19.37
    204. r19.37v
    205. r19.37vOLD
    206. r19.40
    207. r19.41v
    208. r19.41
    209. r19.41vv
    210. r19.42v
    211. r19.43
    212. r19.44v
    213. r19.45v
    214. ralcom
    215. rexcom
    216. rexcomOLD
    217. ralcomf
    218. rexcomf
    219. ralcom13
    220. rexcom13
    221. ralrot3
    222. rexrot4
    223. ralcom2
    224. ralcom3
    225. reeanlem
    226. reean
    227. reeanv
    228. 3reeanv
    229. 2ralor
    230. nfreu1
    231. nfrmo1
    232. nfreud
    233. nfrmod
    234. nfreuw
    235. nfrmow
    236. nfreu
    237. nfrmo
    238. rabid
    239. rabrab
    240. rabidim1
    241. rabid2
    242. rabid2f
    243. rabbi
    244. nfrab1
    245. nfrabw
    246. nfrab
    247. reubida
    248. reubidva
    249. reubidv
    250. reubiia
    251. reubii
    252. rmobida
    253. rmobidva
    254. rmobidv
    255. rmobiia
    256. rmobii
    257. raleqf
    258. rexeqf
    259. reueq1f
    260. rmoeq1f
    261. raleqbidv
    262. rexeqbidv
    263. raleqbi1dv
    264. rexeqbi1dv
    265. raleq
    266. rexeq
    267. reueq1
    268. rmoeq1
    269. raleqi
    270. rexeqi
    271. raleqdv
    272. rexeqdv
    273. reueqd
    274. rmoeqd
    275. raleqbid
    276. rexeqbid
    277. raleqbidva
    278. rexeqbidva
    279. raleleq
    280. raleleqALT
    281. mormo
    282. reu5
    283. reurex
    284. 2reu2rex
    285. reurmo
    286. rmo5
    287. nrexrmo
    288. reueubd
    289. cbvralfw
    290. cbvralfwOLD
    291. cbvrexfw
    292. cbvralf
    293. cbvrexf
    294. cbvralw
    295. cbvrexw
    296. cbvreuw
    297. cbvrmow
    298. cbvrmowOLD
    299. cbvral
    300. cbvrex
    301. cbvreu
    302. cbvrmo
    303. cbvralvw
    304. cbvrexvw
    305. cbvreuvw
    306. cbvralv
    307. cbvrexv
    308. cbvreuv
    309. cbvrmov
    310. cbvraldva2
    311. cbvrexdva2
    312. cbvrexdva2OLD
    313. cbvraldva
    314. cbvrexdva
    315. cbvral2vw
    316. cbvrex2vw
    317. cbvral3vw
    318. cbvral2v
    319. cbvrex2v
    320. cbvral3v
    321. cbvralsvw
    322. cbvrexsvw
    323. cbvralsv
    324. cbvrexsv
    325. sbralie
    326. rabbiia
    327. rabbii
    328. rabbida
    329. rabbid
    330. rabbidva2
    331. rabbia2
    332. rabbidva
    333. rabbidvaOLD
    334. rabbidv
    335. rabeqf
    336. rabeqi
    337. rabeq
    338. rabeqdv
    339. rabeqbidv
    340. rabeqbidva
    341. rabeq2i
    342. rabswap
    343. cbvrabw
    344. cbvrab
    345. cbvrabv
    346. cbvrabvOLD
    347. 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. vtoclgOLD
    76. vtoclbg
    77. vtocl2gf
    78. vtocl3gf
    79. vtocl2g
    80. vtoclgaf
    81. vtoclga
    82. vtocl2ga
    83. vtocl2gaf
    84. vtocl3gaf
    85. vtocl3ga
    86. vtocl4g
    87. vtocl4ga
    88. vtocleg
    89. vtoclegft
    90. vtoclef
    91. vtocle
    92. vtoclri
    93. spcimgft
    94. spcgft
    95. spcimgf
    96. spcimegf
    97. spcgf
    98. spcegf
    99. spcimdv
    100. spcdv
    101. spcimedv
    102. spcgv
    103. spcgvOLD
    104. spcegv
    105. spcegvOLD
    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. rspcv
    126. rspcvOLD
    127. rspccv
    128. rspcva
    129. rspccva
    130. rspcev
    131. rspcevOLD
    132. rspcdva
    133. rspcedvd
    134. rspcime
    135. rspceaimv
    136. rspcedeq1vd
    137. rspcedeq2vd
    138. rspc2
    139. rspc2gv
    140. rspc2v
    141. rspc2va
    142. rspc2ev
    143. rspc3v
    144. rspc3ev
    145. rspceeqv
    146. ralxpxfr2d
    147. rexraleqim
    148. eqvincg
    149. eqvinc
    150. eqvincf
    151. alexeqg
    152. ceqex
    153. ceqsexg
    154. ceqsexgv
    155. ceqsexgvOLD
    156. ceqsrexv
    157. ceqsrexbv
    158. ceqsrex2v
    159. clel2g
    160. clel2
    161. clel3g
    162. clel3
    163. clel4
    164. clel5
    165. pm13.183
    166. rr19.3v
    167. rr19.28v
    168. elabgt
    169. elabgf
    170. elabf
    171. elabgw
    172. elab2gw
    173. elabg
    174. elab
    175. elab2g
    176. elabd
    177. elab2
    178. elab4g
    179. elab3gf
    180. elab3g
    181. elab3
    182. elrabi
    183. elrabf
    184. rabtru
    185. rabeqc
    186. elrab3t
    187. elrab
    188. elrab3
    189. elrabd
    190. elrab2
    191. ralab
    192. ralrab
    193. rexab
    194. rexrab
    195. ralab2
    196. ralab2OLD
    197. ralrab2
    198. rexab2
    199. rexab2OLD
    200. rexrab2
    201. abidnf
    202. dedhb
    203. nelrdva
    204. eqeu
    205. moeq
    206. eueq
    207. eueqi
    208. eueq2
    209. eueq3
    210. moeq3
    211. mosub
    212. mo2icl
    213. mob2
    214. moi2
    215. mob
    216. moi
    217. morex
    218. euxfr2w
    219. euxfrw
    220. euxfr2
    221. euxfr
    222. euind
    223. reu2
    224. reu6
    225. reu3
    226. reu6i
    227. eqreu
    228. rmo4
    229. reu4
    230. reu7
    231. reu8
    232. rmo3f
    233. rmo4f
    234. reu2eqd
    235. reueq
    236. rmoeq
    237. rmoan
    238. rmoim
    239. rmoimia
    240. rmoimi
    241. rmoimi2
    242. 2reu5a
    243. reuimrmo
    244. 2reuswap
    245. 2reuswap2
    246. reuxfrd
    247. reuxfr
    248. reuxfr1d
    249. reuxfr1ds
    250. reuxfr1
    251. reuind
    252. 2rmorex
    253. 2reu5lem1
    254. 2reu5lem2
    255. 2reu5lem3
    256. 2reu5
    257. 2reurex
    258. 2reurmo
    259. 2rmoswap
    260. 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. sbcng
    48. sbcimg
    49. sbcan
    50. sbcor
    51. sbcbig
    52. sbcn1
    53. sbcim1
    54. sbcbid
    55. sbcbidv
    56. sbcbidvOLD
    57. sbcbii
    58. sbcbi1
    59. sbcbi2
    60. sbcbi2OLD
    61. sbcal
    62. sbcex2
    63. sbceqal
    64. sbeqalb
    65. eqsbc3r
    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. 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
  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
    20. elin
  12. 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. sseldi
    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. eqimss
    75. eqimss2
    76. eqimssi
    77. eqimss2i
    78. nssne1
    79. nssne2
    80. nss
    81. nelss
    82. ssrexf
    83. ssrmof
    84. ssralv
    85. ssrexv
    86. ss2ralv
    87. ss2rexv
    88. ralss
    89. rexss
    90. ss2ab
    91. abss
    92. ssab
    93. ssabral
    94. ss2abi
    95. ss2abdv
    96. abssdv
    97. abssi
    98. ss2rab
    99. rabss
    100. ssrab
    101. ssrabdv
    102. rabssdv
    103. ss2rabdv
    104. ss2rabi
    105. rabss2
    106. ssab2
    107. ssrab2
    108. ssrab3
    109. rabssrabd
    110. ssrabeq
    111. rabssab
    112. uniiunlem
    113. dfpss2
    114. dfpss3
    115. psseq1
    116. psseq2
    117. psseq1i
    118. psseq2i
    119. psseq12i
    120. psseq1d
    121. psseq2d
    122. psseq12d
    123. pssss
    124. pssne
    125. pssssd
    126. pssned
    127. sspss
    128. pssirr
    129. pssn2lp
    130. sspsstri
    131. ssnpss
    132. psstr
    133. sspsstr
    134. psssstr
    135. psstrd
    136. sspsstrd
    137. psssstrd
    138. npss
    139. ssnelpss
    140. ssnelpssd
    141. 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. dfnul3
    5. noel
    6. nel02
    7. n0i
    8. ne0i
    9. ne0d
    10. n0ii
    11. ne0ii
    12. vn0
    13. eq0f
    14. neq0f
    15. n0f
    16. eq0
    17. neq0
    18. n0
    19. nel0
    20. reximdva0
    21. rspn0
    22. n0rex
    23. ssn0rex
    24. n0moeu
    25. rex0
    26. reu0
    27. rmo0
    28. 0el
    29. n0el
    30. eqeuel
    31. ssdif0
    32. difn0
    33. pssdifn0
    34. pssdif
    35. ndisj
    36. difin0ss
    37. inssdif0
    38. difid
    39. difidALT
    40. dif0
    41. ab0
    42. dfnf5
    43. ab0orv
    44. abn0
    45. rab0
    46. rabeq0
    47. rabn0
    48. rabxm
    49. rabnc
    50. elneldisj
    51. elnelun
    52. un0
    53. in0
    54. 0un
    55. 0in
    56. inv1
    57. unv
    58. 0ss
    59. ss0b
    60. ss0
    61. sseq0
    62. ssn0
    63. 0dif
    64. abf
    65. eq0rdv
    66. csbprc
    67. csb0
    68. sbcel12
    69. sbceqg
    70. sbceqi
    71. sbcnel12g
    72. sbcne12
    73. sbcel1g
    74. sbceq1g
    75. sbcel2
    76. sbceq2g
    77. csbcom
    78. sbcnestgfw
    79. csbnestgfw
    80. sbcnestgw
    81. csbnestgw
    82. sbcco3gw
    83. sbcnestgf
    84. csbnestgf
    85. sbcnestg
    86. csbnestg
    87. sbcco3g
    88. csbco3g
    89. csbnest1g
    90. csbidm
    91. csbvarg
    92. csbvargi
    93. sbccsb
    94. sbccsb2
    95. rspcsbela
    96. sbnfc2
    97. csbab
    98. csbun
    99. csbin
    100. csbie2df
    101. 2nreu
    102. un00
    103. vss
    104. 0pss
    105. npss0
    106. pssv
    107. disj
    108. disjr
    109. disj1
    110. reldisj
    111. disj3
    112. disjne
    113. disjeq0
    114. disjel
    115. disj2
    116. disj4
    117. ssdisj
    118. disjpss
    119. undisj1
    120. undisj2
    121. ssindif0
    122. inelcm
    123. minel
    124. undif4
    125. disjssun
    126. vdif0
    127. difrab0eq
    128. pssnel
    129. disjdif
    130. difin0
    131. unvdif
    132. undif1
    133. undif2
    134. undifabs
    135. inundif
    136. disjdif2
    137. difun2
    138. undif
    139. ssdifin0
    140. ssdifeq0
    141. ssundif
    142. difcom
    143. pssdifcom1
    144. pssdifcom2
    145. difdifdir
    146. uneqdifeq
    147. raldifeq
    148. r19.2z
    149. r19.2zb
    150. r19.3rz
    151. r19.28z
    152. r19.3rzv
    153. r19.9rzv
    154. r19.28zv
    155. r19.37zv
    156. r19.45zv
    157. r19.44zv
    158. r19.27z
    159. r19.27zv
    160. r19.36zv
    161. rzal
    162. rexn0
    163. ralidm
    164. ral0
    165. ralf0
    166. ralnralall
    167. falseral0
    168. raaan
    169. raaanv
    170. sbss
    171. sbcssg
    172. raaan2
    173. 2reu4lem
    174. 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. elpwg
    5. elpw
    6. velpw
    7. elpwOLD
    8. elpwgOLD
    9. elpwd
    10. elpwi
    11. elpwb
    12. elpwid
    13. elelpwi
    14. sspw
    15. sspwi
    16. sspwd
    17. pweq
    18. pweqALT
    19. pweqi
    20. pweqd
    21. pwunss
    22. nfpw
    23. pwidg
    24. pwidb
    25. pwid
    26. pwss
    27. pwundif
  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. 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. ralsnsg
    46. rexsns
    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. opeq1OLD
    242. opeq2
    243. opeq2OLD
    244. opeq12
    245. opeq1i
    246. opeq2i
    247. opeq12i
    248. opeq1d
    249. opeq2d
    250. opeq12d
    251. oteq1
    252. oteq2
    253. oteq3
    254. oteq1d
    255. oteq2d
    256. oteq3d
    257. oteq123d
    258. nfop
    259. nfopd
    260. csbopg
    261. opidg
    262. opid
    263. ralunsn
    264. 2ralunsn
    265. opprc
    266. opprc1
    267. opprc2
    268. oprcl
    269. pwsn
    270. pwsnOLD
    271. pwpr
    272. pwtp
    273. pwpwpw0
    274. pwv
    275. prproe
    276. 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. uniss
    10. unissi
    11. unissd
    12. unieq
    13. unieqOLD
    14. unieqi
    15. unieqd
    16. eluniab
    17. elunirab
    18. unipr
    19. uniprg
    20. unisng
    21. unisn
    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
  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