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
|- 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 ) )