Mathbox for Norm Megill 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > alequcomX  Unicode version 
Description: Commutation law for identical variable specifiers. The antecedent and consequent are true when and are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5Aug1993.) 
Ref  Expression 

alequcomX 
Step  Hyp  Ref  Expression 

1  ax10 1678  1 
Colors of variables: wff set class 
Syntax hints: wi 6 wal 1532 
This theorem was proved from axioms: ax10 1678 
Copyright terms: Public domain  W3C validator 