Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > stdpc6  Unicode version 
Description: One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1870.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain). (Contributed by NM, 16Feb2005.) 
Ref  Expression 

stdpc6 
Step  Hyp  Ref  Expression 

1  equid 1662  . 2  
2  1  axgen 1536  1 
Colors of variables: wff set class 
Syntax hints: wal 1530 
This theorem is referenced by: cbv3h 1936 cbv3hwAUX7 29493 cbv3hOLD7 29678 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 axgen 1536 ax5 1547 ax17 1606 ax9 1644 ax8 1661 
Copyright terms: Public domain  W3C validator 