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)