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 1686. 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.) (Proof shortened by Wolf Lammen, 1Jan2018.) 
Ref  Expression 

stdpc5.1 
Ref  Expression 

stdpc5 
Step  Hyp  Ref  Expression 

1  stdpc5.1  . . 3  
2  1  19.21 1810  . 2 
3  2  biimpi 187  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wal 1546 wnf 1550 
This theorem is referenced by: ra5 3202 ax10ext 27291 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1552 ax5 1563 ax17 1623 ax9 1662 ax8 1683 ax6 1740 ax11 1757 
This theorem depends on definitions: dfbi 178 dfex 1548 dfnf 1551 
Copyright terms: Public domain  W3C validator 