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 2102. 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 1743  . 2 
3  alim 1546  . 2  
4  2, 3  syl5 30  1 
Colors of variables: wff set class 
Syntax hints: wi 6 wal 1528 wnf 1532 
This theorem is referenced by: ra5 3076 ax10ext 27005 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 axgen 1534 ax5 1545 ax17 1604 ax9 1637 ax8 1645 ax11 1716 
This theorem depends on definitions: dfbi 179 dfnf 1533 
Copyright terms: Public domain  W3C validator 