Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > ax10  Structured version GIF version 
Description: Axiom of Quantifier
Substitution. One of the equality and substitution
axioms of predicate calculus with equality. Appears as Lemma L12 in
[Megill] p. 445 (p. 12 of the preprint).
The original version of this axiom was ax10o 1522 ("o" for "old") and was replaced with this shorter ax10 1334 in May 2008. The old axiom is proved from this one as theorem ax10o 1521. Conversely, this axiom is proved from ax10o 1522 as theorem ax10 1523. (Contributed by NM, 5Aug1993.) 
Ref  Expression 

ax10  ⊢ (∀x x = y → ∀y y = x) 
Step  Hyp  Ref  Expression 

1  vx  . . . 4 set x  
2  vy  . . . 4 set y  
3  1, 2  weq 1330  . . 3 wff x = y 
4  3, 1  wal 1271  . 2 wff ∀x x = y 
5  2, 1  weq 1330  . . 3 wff y = x 
6  5, 2  wal 1271  . 2 wff ∀y y = x 
7  4, 6  wi 4  1 wff (∀x x = y → ∀y y = x) 
Colors of variables: wff set class 
This axiom is referenced by: alequcom 1345 ax10o 1521 naecoms 1530 
Copyright terms: Public domain  W3C validator 