Metamath Proof Explorer

Table of Contents - 21.20.4. First-order logic

Utility lemmas or strengthenings of theorems in the main part (biconditional or closed forms, or fewer disjoint variable conditions, or disjoint variable conditions replaced with nonfreeness hypotheses...). Sorted in the same order as in the main part.

1. Universal and existential quantifiers, nonfreeness predicate
2. Adding ax-gen
   1. bj-genr
   2. bj-genl
   3. bj-genan
   4. bj-mpgs
3. Adding ax-4
   1. bj-2alim
   2. bj-2exim
   3. bj-alanim
   4. bj-2albi
   5. bj-notalbii
   6. bj-2exbi
   7. bj-3exbi
   8. bj-sylggt
   9. bj-sylgt2
   10. bj-alrimg
   11. bj-alrimd
   12. bj-sylget
   13. bj-sylget2
   14. bj-exlimg
   15. bj-sylge
   16. bj-exlimd
   17. bj-nfimexal
   18. bj-alexim
   19. bj-nexdh
   20. bj-nexdh2
   21. bj-hbxfrbi
   22. bj-hbyfrbi
   23. bj-exalim
   24. bj-exalimi
   25. bj-exalims
   26. bj-exalimsi
   27. bj-ax12ig
   28. bj-ax12i
   29. bj-nfimt
   30. bj-cbvalimt
   31. bj-cbveximt
   32. bj-eximALT
   33. bj-aleximiALT
   34. bj-eximcom
4. Adding ax-5
   1. bj-ax12wlem
   2. bj-cbvalim
   3. bj-cbvexim
   4. bj-cbvalimi
   5. bj-cbveximi
   6. bj-cbval
   7. bj-cbvex
   8. wmoo
   9. df-bj-mo
5. Equality and substitution
   1. bj-df-sb
   2. bj-ssbeq
   3. bj-ssblem1
   4. bj-ssblem2
   5. bj-ax12v
   6. bj-ax12
   7. bj-ax12ssb
   8. bj-19.41al
   9. bj-equsexval
   10. bj-subst
   11. bj-ssbid2
   12. bj-ssbid2ALT
   13. bj-ssbid1
   14. bj-ssbid1ALT
   15. bj-ax6elem1
   16. bj-ax6elem2
   17. bj-ax6e
6. Adding ax-6
   1. bj-spimvwt
   2. bj-spnfw
   3. bj-cbvexiw
   4. bj-cbvexivw
   5. bj-modald
   6. bj-denot
   7. bj-eqs
7. Adding ax-7
   1. bj-cbvexw
   2. bj-ax12w
8. Membership predicate, ax-8 and ax-9
   1. bj-ax89
   2. bj-cleljusti
9. Logical redundancy of ax-10--13
10. Adding ax-10
11. Adding ax-11
    1. bj-alcomexcom
    2. bj-hbalt
12. Adding ax-12
    1. axc11n11
    2. axc11n11r
    3. bj-axc16g16
    4. bj-ax12v3
    5. bj-ax12v3ALT
    6. bj-sb
    7. bj-modalbe
    8. bj-spst
    9. bj-19.21bit
    10. bj-19.23bit
    11. bj-nexrt
    12. bj-alrim
    13. bj-alrim2
    14. bj-nfdt0
    15. bj-nfdt
    16. bj-nexdt
    17. bj-nexdvt
    18. bj-alexbiex
    19. bj-exexbiex
    20. bj-alalbial
    21. bj-exalbial
    22. bj-19.9htbi
    23. bj-hbntbi
    24. bj-biexal1
    25. bj-biexal2
    26. bj-biexal3
    27. bj-bialal
    28. bj-biexex
    29. bj-hbext
    30. bj-nfalt
    31. bj-nfext
    32. bj-eeanvw
    33. bj-modal4
    34. bj-modal4e
    35. bj-modalb
    36. bj-wnf1
    37. bj-wnf2
    38. bj-wnfanf
    39. bj-wnfenf
    40. bj-substax12
    41. bj-substw
13. Really adding ax-12
14. Nonfreeness
    1. wnnf
    2. df-bj-nnf
    3. bj-nnfbi
    4. bj-nnfbd
    5. bj-nnfbii
    6. bj-nnfa
    7. bj-nnfad
    8. bj-nnfai
    9. bj-nnfe
    10. bj-nnfed
    11. bj-nnfei
    12. bj-nnfea
    13. bj-nnfead
    14. bj-nnfeai
    15. bj-dfnnf2
    16. bj-nnfnfTEMP
    17. bj-wnfnf
    18. bj-nnfnt
    19. bj-nnftht
    20. bj-nnfth
    21. bj-nnfnth
    22. bj-nnfim1
    23. bj-nnfim2
    24. bj-nnfim
    25. bj-nnfimd
    26. bj-nnfan
    27. bj-nnfand
    28. bj-nnfor
    29. bj-nnford
    30. bj-nnfbit
    31. bj-nnfbid
    32. bj-nnfv
    33. bj-nnf-alrim
    34. bj-nnf-exlim
    35. bj-dfnnf3
    36. bj-nfnnfTEMP
    37. bj-nnfa1
    38. bj-nnfe1
    39. bj-19.12
    40. bj-nnflemaa
    41. bj-nnflemee
    42. bj-nnflemae
    43. bj-nnflemea
    44. bj-nnfalt
    45. bj-nnfext
    46. bj-stdpc5t
    47. bj-19.21t
    48. bj-19.23t
    49. bj-19.36im
    50. bj-19.37im
    51. bj-19.42t
    52. bj-19.41t
    53. bj-sbft
    54. bj-pm11.53vw
    55. bj-pm11.53v
    56. bj-pm11.53a
    57. bj-equsvt
    58. bj-equsalvwd
    59. bj-equsexvwd
    60. bj-sbievwd
15. Adding ax-13
    1. bj-axc10
    2. bj-alequex
    3. bj-spimt2
    4. bj-cbv3ta
    5. bj-cbv3tb
    6. bj-hbsb3t
    7. bj-hbsb3
    8. bj-nfs1t
    9. bj-nfs1t2
    10. bj-nfs1
16. Removing dependencies on ax-13 (and ax-11)
    1. bj-axc10v
    2. bj-spimtv
    3. bj-cbv3hv2
    4. bj-cbv1hv
    5. bj-cbv2hv
    6. bj-cbv2v
    7. bj-cbvaldv
    8. bj-cbvexdv
    9. bj-cbval2vv
    10. bj-cbvex2vv
    11. bj-cbvaldvav
    12. bj-cbvexdvav
    13. bj-cbvex4vv
    14. bj-equsalhv
    15. bj-axc11nv
    16. bj-aecomsv
    17. bj-axc11v
    18. bj-drnf2v
    19. bj-equs45fv
    20. bj-hbs1
    21. bj-nfs1v
    22. bj-hbsb2av
    23. bj-hbsb3v
    24. bj-nfsab1
    25. bj-dtrucor2v
17. Strengthenings of theorems of the main part
18. Distinct var metavariables
    1. bj-hbaeb2
    2. bj-hbaeb
    3. bj-hbnaeb
    4. bj-dvv
19. Around ~ equsal
    1. bj-equsal1t
    2. bj-equsal1ti
    3. bj-equsal1
    4. bj-equsal2
    5. bj-equsal
20. Some Principia Mathematica proofs
    1. stdpc5t
    2. bj-stdpc5
    3. 2stdpc5
    4. bj-19.21t0
    5. exlimii
    6. ax11-pm
    7. ax6er
    8. exlimiieq1
    9. exlimiieq2
    10. ax11-pm2
21. Alternate definition of substitution
    1. bj-sbsb
    2. bj-dfsb2
22. Lemmas for substitution
    1. bj-sbf3
    2. bj-sbf4
23. Existential uniqueness
    1. bj-eu3f
24. First-order logic: miscellaneous
    1. bj-sblem1
    2. bj-sblem2
    3. bj-sblem
    4. bj-sbievw1
    5. bj-sbievw2
    6. bj-sbievw
    7. bj-sbievv
    8. bj-moeub
    9. bj-sbidmOLD
    10. bj-dvelimdv
    11. bj-dvelimdv1
    12. bj-dvelimv
    13. bj-nfeel2
    14. bj-axc14nf
    15. bj-axc14
    16. mobidvALT
    17. sbn1ALT