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	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜓 ) → ( 𝜑 → ∀ 𝑥 𝜓 ) )