Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > stdpc6  Structured version GIF version 
Description: One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1650.) 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  ⊢ ∀x x = x 
Step  Hyp  Ref  Expression 

1  equid 1586  . 2 ⊢ x = x  
2  1  axgen 1335  1 ⊢ ∀x x = x 
Colors of variables: wff set class 
Syntax hints: ∀wal 1240 
This theorem was proved from axioms: ax1 5 ax2 6 axmp 7 axia1 99 axgen 1335 axie2 1380 ax8 1392 ax17 1416 axi9 1420 
This theorem depends on definitions: dfbi 110 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 