Metamath Proof Explorer


Table of Contents - 20.16.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-sylgt2
    9. bj-alrimg
    10. bj-alrimd
    11. bj-sylget
    12. bj-sylget2
    13. bj-exlimg
    14. bj-sylge
    15. bj-exlimd
    16. bj-nfimexal
    17. bj-alexim
    18. bj-nexdh
    19. bj-nexdh2
    20. bj-hbxfrbi
    21. bj-hbyfrbi
    22. bj-exalim
    23. bj-exalimi
    24. bj-exalims
    25. bj-exalimsi
    26. bj-ax12ig
    27. bj-ax12i
    28. bj-nfimt
    29. bj-cbvalimt
    30. bj-cbveximt
    31. bj-eximALT
    32. bj-aleximiALT
    33. 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-ssbeq
    2. bj-ssblem1
    3. bj-ssblem2
    4. bj-ax12v
    5. bj-ax12
    6. bj-ax12ssb
    7. bj-19.41al
    8. bj-equsexval
    9. bj-subst
    10. bj-ssbid2
    11. bj-ssbid2ALT
    12. bj-ssbid1
    13. bj-ssbid1ALT
    14. bj-ax6elem1
    15. bj-ax6elem2
    16. 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-elequ12
    3. 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-dtru
    26. 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
    3. bj-sbnf
  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