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

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

Proof of Theorem aecoms
StepHypRef Expression
1 aecom 1899 . 2  |-  ( A. y  y  =  x  ->  A. x  x  =  y )
2 alequcoms.1 . 2  |-  ( A. x  x  =  y  ->  ph )
31, 2syl 15 1  |-  ( A. y  y  =  x  ->  ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530
This theorem is referenced by:  hbae  1906  dvelimh  1917  dral1  1918  nd4  8228  axrepnd  8232  axpowndlem3  8237  axpownd  8239  axregnd  8242  axinfnd  8244  axacndlem5  8249  axacnd  8250  e2ebind  28628  a12stdy4  29751
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
  Copyright terms: Public domain W3C validator