Metamath Proof Explorer


Table of Contents - 20.16.5. Set theory

  1. Eliminability of class terms
    1. eliminable1
    2. eliminable2a
    3. eliminable2b
    4. eliminable2c
    5. eliminable3a
    6. eliminable3b
    7. eliminable-velab
    8. eliminable-veqab
    9. eliminable-abeqv
    10. eliminable-abeqab
    11. eliminable-abelv
    12. eliminable-abelab
  2. Classes without the axiom of extensionality
    1. bj-denoteslem
    2. bj-denotes
    3. bj-issettru
    4. bj-elabtru
    5. bj-issetwt
    6. bj-issetw
    7. bj-elissetv
    8. bj-elisset
    9. bj-issetiv
    10. bj-isseti
    11. bj-ralvw
    12. bj-rexvw
    13. bj-rababw
    14. bj-rexcom4bv
    15. bj-rexcom4b
    16. bj-ceqsalt0
    17. bj-ceqsalt1
    18. bj-ceqsalt
    19. bj-ceqsaltv
    20. bj-ceqsalg0
    21. bj-ceqsalg
    22. bj-ceqsalgALT
    23. bj-ceqsalgv
    24. bj-ceqsalgvALT
    25. bj-ceqsal
    26. bj-ceqsalv
    27. bj-spcimdv
    28. bj-spcimdvv
  3. Characterization among sets versus among classes
    1. elelb
    2. bj-pwvrelb
  4. The nonfreeness quantifier for classes
    1. bj-nfcsym
  5. Proposal for the definitions of class membership and class equality
    1. bj-ax9
  6. Lemmas for class substitution
    1. bj-sbeqALT
    2. bj-sbeq
    3. bj-sbceqgALT
    4. bj-csbsnlem
    5. bj-csbsn
    6. bj-sbel1
    7. bj-abv
    8. bj-ab0
    9. bj-abf
    10. bj-csbprc
  7. Removing some axiom requirements and disjoint variable conditions
    1. bj-exlimvmpi
    2. bj-exlimmpi
    3. bj-exlimmpbi
    4. bj-exlimmpbir
    5. bj-vtoclf
    6. bj-vtocl
    7. bj-vtoclg1f1
    8. bj-vtoclg1f
    9. bj-vtoclg1fv
    10. bj-vtoclg
    11. bj-rabbida2
    12. bj-rabeqd
    13. bj-rabeqbid
    14. bj-rabeqbida
    15. bj-seex
    16. bj-nfcf
    17. bj-zfauscl
  8. Class abstractions
    1. bj-unrab
    2. bj-inrab
    3. bj-inrab2
    4. bj-inrab3
    5. bj-rabtr
    6. bj-rabtrALT
    7. bj-rabtrAUTO
  9. Restricted nonfreeness
    1. wrnf
    2. df-bj-rnf
  10. Russell's paradox
    1. bj-ru0
    2. bj-ru1
    3. bj-ru
  11. Curry's paradox in set theory
    1. currysetlem
    2. curryset
    3. currysetlem1
    4. currysetlem2
    5. currysetlem3
    6. currysetALT
  12. Some disjointness results
    1. bj-n0i
    2. bj-disjcsn
    3. bj-disjsn01
    4. bj-0nel1
    5. bj-1nel0
  13. Complements on direct products
    1. bj-xpimasn
    2. bj-xpima1sn
    3. bj-xpima1snALT
    4. bj-xpima2sn
    5. bj-xpnzex
    6. bj-xpexg2
    7. bj-xpnzexb
    8. bj-cleq
  14. "Singletonization" and tagging
    1. bj-snsetex
    2. bj-clex
    3. bj-csngl
    4. df-bj-sngl
    5. bj-sngleq
    6. bj-elsngl
    7. bj-snglc
    8. bj-snglss
    9. bj-0nelsngl
    10. bj-snglinv
    11. bj-snglex
    12. bj-ctag
    13. df-bj-tag
    14. bj-tageq
    15. bj-eltag
    16. bj-0eltag
    17. bj-tagn0
    18. bj-tagss
    19. bj-snglsstag
    20. bj-sngltagi
    21. bj-sngltag
    22. bj-tagci
    23. bj-tagcg
    24. bj-taginv
    25. bj-tagex
    26. bj-xtageq
    27. bj-xtagex
  15. Tuples of classes
    1. bj-cproj
    2. df-bj-proj
    3. bj-projeq
    4. bj-projeq2
    5. bj-projun
    6. bj-projex
    7. bj-projval
    8. bj-c1upl
    9. df-bj-1upl
    10. bj-1upleq
    11. bj-cpr1
    12. df-bj-pr1
    13. bj-pr1eq
    14. bj-pr1un
    15. bj-pr1val
    16. bj-pr11val
    17. bj-pr1ex
    18. bj-1uplth
    19. bj-1uplex
    20. bj-1upln0
    21. bj-c2uple
    22. df-bj-2upl
    23. bj-2upleq
    24. bj-pr21val
    25. bj-cpr2
    26. df-bj-pr2
    27. bj-pr2eq
    28. bj-pr2un
    29. bj-pr2val
    30. bj-pr22val
    31. bj-pr2ex
    32. bj-2uplth
    33. bj-2uplex
    34. bj-2upln0
    35. bj-2upln1upl
  16. Set theory: elementary operations relative to a universe
    1. bj-rcleqf
    2. bj-rcleq
    3. bj-reabeq
    4. bj-disj2r
    5. bj-sscon
  17. Set theory: miscellaneous
    1. bj-pw0ALT
    2. bj-sselpwuni
    3. bj-unirel
    4. bj-elpwg
    5. bj-vjust
    6. bj-df-v
    7. bj-df-nul
    8. bj-nul
    9. bj-nuliota
    10. bj-nuliotaALT
    11. bj-vtoclgfALT
    12. bj-elsn12g
    13. bj-elsnb
    14. bj-pwcfsdom
    15. bj-grur1
    16. bj-bm1.3ii
    17. bj-0nelopab
    18. bj-brrelex12ALT
    19. bj-epelg
    20. bj-epelb
    21. bj-nsnid
  18. Evaluation
    1. bj-evaleq
    2. bj-evalfun
    3. bj-evalfn
    4. bj-evalval
    5. bj-evalid
    6. bj-ndxarg
    7. bj-evalidval
  19. Elementwise operations
    1. celwise
    2. df-elwise
  20. Elementwise intersection (families of sets induced on a subset)
    1. bj-rest00
    2. bj-restsn
    3. bj-restsnss
    4. bj-restsnss2
    5. bj-restsn0
    6. bj-restsn10
    7. bj-restsnid
    8. bj-rest10
    9. bj-rest10b
    10. bj-restn0
    11. bj-restn0b
    12. bj-restpw
    13. bj-rest0
    14. bj-restb
    15. bj-restv
    16. bj-resta
    17. bj-restuni
    18. bj-restuni2
    19. bj-restreg
  21. Moore collections (complements)
    1. bj-intss
    2. bj-raldifsn
    3. bj-0int
    4. bj-mooreset
    5. cmoore
    6. df-bj-moore
    7. bj-ismoore
    8. bj-ismoored0
    9. bj-ismoored
    10. bj-ismoored2
    11. bj-ismooredr
    12. bj-ismooredr2
    13. bj-discrmoore
    14. bj-0nmoore
    15. bj-snmoore
    16. bj-snmooreb
    17. bj-prmoore
  22. Maps-to notation for functions with three arguments
    1. bj-0nelmpt
    2. bj-mptval
    3. bj-dfmpoa
    4. bj-mpomptALT
    5. cmpt3
    6. df-bj-mpt3
  23. Currying
    1. csethom
    2. df-bj-sethom
    3. ctophom
    4. df-bj-tophom
    5. cmgmhom
    6. df-bj-mgmhom
    7. ctopmgmhom
    8. df-bj-topmgmhom
    9. ccur-
    10. df-bj-cur
    11. cunc-
    12. df-bj-unc
  24. Setting components of extensible structures
    1. cstrset
    2. df-strset
    3. setsstrset