 Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  stdpc5 Structured version   Visualization version   GIF version

Theorem stdpc5 2039
 Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎ𝑥𝜑 can be thought of as emulating "𝑥 is not free in 𝜑." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example 𝑥 would not (for us) be free in 𝑥 = 𝑥 by nfequid 1890. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. See stdpc5v 1820 for a version requiring fewer axioms. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) Remove dependency on ax-10 1966. (Revised by Wolf Lammen, 4-Jul-2021.)
Hypothesis
Ref Expression
stdpc5.1 𝑥𝜑
Assertion
Ref Expression
stdpc5 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))

Proof of Theorem stdpc5
StepHypRef Expression
1 stdpc5.1 . 2 𝑥𝜑
2 19.21t-1 2034 . 2 (Ⅎ𝑥𝜑 → (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓)))
31, 2ax-mp 5 1 (∀𝑥(𝜑𝜓) → (𝜑 → ∀𝑥𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1472  Ⅎwnf 1698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-12 1983 This theorem depends on definitions:  df-bi 195  df-ex 1695  df-nf 1699 This theorem is referenced by:  2stdpc5  31849
 Copyright terms: Public domain W3C validator