HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem hbae 1700
Description: All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hbae  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1587 . . . . 5  |-  ( A. x  x  =  y  ->  x  =  y )
2 ax-12o 1560 . . . . 5  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  =  y  ->  A. z  x  =  y )
) )
31, 2syl7 63 . . . 4  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( A. x  x  =  y  ->  A. z  x  =  y ) ) )
4 ax10o 1694 . . . . 5  |-  ( A. x  x  =  z  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
54alequcoms 1577 . . . 4  |-  ( A. z  z  =  x  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
6 ax10o 1694 . . . . . . 7  |-  ( A. x  x  =  y  ->  ( A. x  x  =  y  ->  A. y  x  =  y )
)
76pm2.43i 43 . . . . . 6  |-  ( A. x  x  =  y  ->  A. y  x  =  y )
8 ax10o 1694 . . . . . 6  |-  ( A. y  y  =  z  ->  ( A. y  x  =  y  ->  A. z  x  =  y )
)
97, 8syl5 28 . . . . 5  |-  ( A. y  y  =  z  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
109alequcoms 1577 . . . 4  |-  ( A. z  z  =  y  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
113, 5, 10pm2.61ii 155 . . 3  |-  ( A. x  x  =  y  ->  A. z  x  =  y )
1211a5i 1600 . 2  |-  ( A. x  x  =  y  ->  A. x A. z  x  =  y )
13 ax-7 1442 . 2  |-  ( A. x A. z  x  =  y  ->  A. z A. x  x  =  y )
1412, 13syl 15 1  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1439
This theorem is referenced by:  hbaes  1702  hbnae  1703  dral1  1711  dral2  1713  drex2  1716  sbequ5  1752  aev  1770  hbsb4  1817  sbcom  1827  sbcom2  1914  exists1  2036  copsexg  3804  axextnd  7681  axrepnd  7684  axunnd  7686  axpowndlem3  7689  axpownd  7691  axregndlem1  7692  axregnd  7694  axacndlem1  7697  axacndlem2  7698  axacndlem3  7699  axacndlem4  7700  axacndlem5  7701  axacnd  7702  copsexgb  22098  a9e2eq  24890  a12stdy3  26736
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1440  ax-6 1441  ax-7 1442  ax-gen 1443  ax-8 1522  ax-11 1523  ax-17 1527  ax-12o 1560  ax-10 1574  ax-9 1580  ax-4 1587
This theorem depends on definitions:  df-bi 175  df-ex 1445
Copyright terms: Public domain