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

Theorem hbae 1699
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 1586 . . . . 5  |-  ( A. x  x  =  y  ->  x  =  y )
2 ax-12o 1559 . . . . 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 1693 . . . . 5  |-  ( A. x  x  =  z  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
54alequcoms 1576 . . . 4  |-  ( A. z  z  =  x  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
6 ax10o 1693 . . . . . . 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 1693 . . . . . 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 1576 . . . 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 1599 . 2  |-  ( A. x  x  =  y  ->  A. x A. z  x  =  y )
13 ax-7 1441 . 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 1438
This theorem is referenced by:  hbaes  1701  hbnae  1702  dral1  1710  dral2  1712  drex2  1715  sbequ5  1751  aev  1769  hbsb4  1816  sbcom  1826  sbcom2  1913  exists1  2035  copsexg  3802  axextnd  7675  axrepnd  7678  axunnd  7680  axpowndlem3  7683  axpownd  7685  axregndlem1  7686  axregnd  7688  axacndlem1  7691  axacndlem2  7692  axacndlem3  7693  axacndlem4  7694  axacndlem5  7695  axacnd  7696  copsexgb  21610  a9e2eq  24465  a12stdy3  26311
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1439  ax-6 1440  ax-7 1441  ax-gen 1442  ax-8 1521  ax-11 1522  ax-17 1526  ax-12o 1559  ax-10 1573  ax-9 1579  ax-4 1586
This theorem depends on definitions:  df-bi 175  df-ex 1444
Copyright terms: Public domain