Theorem stdpc5 1598

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 1716. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.)

Hypothesis

Ref	Expression
stdpc5.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
stdpc5	⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))

Proof of Theorem stdpc5

Step	Hyp	Ref	Expression
1		stdpc5.1	. . 3 ⊢ Ⅎ𝑥𝜑
2	1	19.21 1597	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
3	2	biimpi 120	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))

Syntax hints:   → wi 4  ∀wal 1362  Ⅎwnf 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-ial 1548  ax-i5r 1549

This theorem depends on definitions:  df-bi 117  df-nf 1475

This theorem is referenced by:  sbalyz  2018  ra5  3078