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-elissetALT
   8. bj-issetiv
   9. bj-isseti
   10. bj-ralvw
   11. bj-rexvw
   12. bj-rababw
   13. bj-rexcom4bv
   14. bj-rexcom4b
   15. bj-ceqsalt0
   16. bj-ceqsalt1
   17. bj-ceqsalt
   18. bj-ceqsaltv
   19. bj-ceqsalg0
   20. bj-ceqsalg
   21. bj-ceqsalgALT
   22. bj-ceqsalgv
   23. bj-ceqsalgvALT
   24. bj-ceqsal
   25. bj-ceqsalv
   26. bj-spcimdv
   27. bj-spcimdvv
3. Characterization among sets versus among classes
   1. elelb
   2. bj-pwvrelb
4. The nonfreeness quantifier for classes
   1. bj-nfcsym
5. 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-abvALT
   9. bj-ab0
   10. bj-abf
   11. bj-csbprc
6. 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
7. Class abstractions
   1. bj-elabd2ALT
   2. bj-unrab
   3. bj-inrab
   4. bj-inrab2
   5. bj-inrab3
   6. bj-rabtr
   7. bj-rabtrALT
   8. bj-rabtrAUTO
8. Generalized class abstractions
   1. bj-cgab
   2. df-bj-gab
   3. bj-gabss
   4. bj-gabssd
   5. bj-gabeqd
   6. bj-gabeqis
   7. bj-elgab
   8. bj-gabima
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. eleq2w2ALT
    2. bj-clel3gALT
    3. bj-pw0ALT
    4. bj-sselpwuni
    5. bj-unirel
    6. bj-elpwg
    7. bj-vjust
    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-dfid2ALT
    18. bj-0nelopab
    19. bj-brrelex12ALT
    20. bj-epelg
    21. bj-epelb
    22. bj-nsnid
    23. bj-rdg0gALT
18. Evaluation at a class
    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-raldifsn
    2. bj-0int
    3. bj-mooreset
    4. cmoore
    5. df-bj-moore
    6. bj-ismoore
    7. bj-ismoored0
    8. bj-ismoored
    9. bj-ismoored2
    10. bj-ismooredr
    11. bj-ismooredr2
    12. bj-discrmoore
    13. bj-0nmoore
    14. bj-snmoore
    15. bj-snmooreb
    16. 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