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 1663. 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 1754  . 2 
3  alim 1548  . 2  
4  2, 3  syl5 28  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wal 1530 wnf 1534 
This theorem is referenced by: ra5 3088 ax10ext 27709 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1536 ax5 1547 ax17 1606 ax9 1644 ax8 1661 ax11 1727 
This theorem depends on definitions: dfbi 177 dfnf 1535 
Copyright terms: Public domain  W3C validator 