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

Theorem hbae 1720
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 1606 . . . . 5  |-  ( A. x  x  =  y  ->  x  =  y )
2 ax-12o 1578 . . . . 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 1714 . . . . 5  |-  ( A. x  x  =  z  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
54alequcoms 1595 . . . 4  |-  ( A. z  z  =  x  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
6 ax10o 1714 . . . . . . 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 1714 . . . . . 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 1595 . . . 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 1619 . 2  |-  ( A. x  x  =  y  ->  A. x A. z  x  =  y )
13 ax-7 1453 . 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 1450
This theorem is referenced by:  hbaes  1722  hbnae  1723  dral1  1731  dral2  1733  drex2  1736  sbequ5  1772  aev  1790  hbsb4  1837  sbcom  1847  sbcom2  1934  exists1  2056  copsexg  3820  axextnd  7665  axrepnd  7668  axunndlem1  7669  axunnd  7670  axpowndlem3  7673  axpownd  7675  axregndlem1  7676  axregnd  7678  axacndlem1  7681  axacndlem2  7682  axacndlem3  7683  axacndlem4  7684  axacndlem5  7685  axacnd  7686  copsexgb  21530  a9e2eq  24374  a12stdy3  26220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1451  ax-6 1452  ax-7 1453  ax-gen 1454  ax-8 1540  ax-11 1541  ax-17 1545  ax-12o 1578  ax-10 1592  ax-9 1598  ax-4 1606
This theorem depends on definitions:  df-bi 175  df-ex 1456
Copyright terms: Public domain