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 1645. 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 1742  . 2 
3  alim 1545  . 2  
4  2, 3  syl5 28  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wal 1527 wnf 1531 
This theorem is referenced by: ra5 3075 ax10ext 27606 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1533 ax5 1544 ax17 1603 ax9 1635 ax8 1643 ax11 1715 
This theorem depends on definitions: dfbi 177 dfnf 1532 
Copyright terms: Public domain  W3C validator 