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	$$⊢Ⅎx\phi$$
Assertion	stdpc5	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\phi \to \forall x\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		stdpc5.1	$$⊢Ⅎx\phi$$
2	1	19.21	$$⊢\forall x\left(\phi \to \psi \right)\leftrightarrow \left(\phi \to \forall x\psi \right)$$
3	2	biimpi	$$⊢\forall x\left(\phi \to \psi \right)\to \left(\phi \to \forall x\psi \right)$$