MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  aecoms Structured version   Unicode version

Theorem aecoms 2037
Description: A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
aecoms.1  |-  ( A. x  x  =  y  ->  ph )
Assertion
Ref Expression
aecoms  |-  ( A. y  y  =  x  ->  ph )

Proof of Theorem aecoms
StepHypRef Expression
1 ax10 2026 . 2  |-  ( A. y  y  =  x  ->  A. x  x  =  y )
2 aecoms.1 . 2  |-  ( A. x  x  =  y  ->  ph )
31, 2syl 16 1  |-  ( A. y  y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1550
This theorem is referenced by:  ax10o  2039  hbaeOLD  2042  dral1OLD  2059  dvelimhOLD  2073  nd4  8467  axrepnd  8471  axpowndlem3  8476  axpownd  8478  axregnd  8481  axinfnd  8483  axacndlem5  8488  axacnd  8489  e2ebind  28652
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator