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	|- F/ x ph
Assertion	stdpc5	|- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )

Proof

Step	Hyp	Ref	Expression
1		stdpc5.1	|- F/ x ph
2	1	19.21	|- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) )
3	2	biimpi	|- ( A. x ( ph -> ps ) -> ( ph -> A. x ps ) )