Theorem stdpc5 2248

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 2048. 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 1973 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 2180. (Revised by Wolf Lammen, 4-Jul-2021.) (Proof shortened by Wolf Lammen, 11-Oct-2021.)

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 2247	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓))
3	2	biimpi 219	1 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓))

This proof depends on syntax axioms:   → wi 4  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-12 2216

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817

This theorem is used by:  2stdpc5  37918