Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > stdpc5  Unicode version 
Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis can be thought of as emulating " is not free in ." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example would not (for us) be free in by nfequid 1688. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22Sep1993.) (Revised by Mario Carneiro, 12Oct2016.) 
Ref  Expression 

stdpc5.1 
Ref  Expression 

stdpc5 
Step  Hyp  Ref  Expression 

1  stdpc5.1  . . 3  
2  1  nfri 1703  . 2 
3  alim 1548  . 2  
4  2, 3  syl5 30  1 
Colors of variables: wff set class 
Syntax hints: wi 6 wal 1532 wnf 1539 
This theorem is referenced by: ra5 3036 ax10ext 26959 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 ax5 1533 ax4 1692 
This theorem depends on definitions: dfbi 179 dfnf 1540 
Copyright terms: Public domain  W3C validator 