Metamath Proof Explorer


Theorem stdpc5

Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of Mendelson p. 69. The hypothesis F/ x ph can be thought of as emulating " x is not free in ph ". With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example x would not (for us) be free in x = x by nfequid . 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 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 . (Revised by Wolf Lammen, 4-Jul-2021) (Proof shortened by Wolf Lammen, 11-Oct-2021)

Ref Expression
Hypothesis stdpc5.1 𝑥 𝜑
Assertion stdpc5 ( ∀ 𝑥 ( 𝜑𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜓 ) )

Proof

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