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

Theorem hbae 1702
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 1589 . . . . 5  |-  ( A. x  x  =  y  ->  x  =  y )
2 ax-12o 1562 . . . . 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 1696 . . . . 5  |-  ( A. x  x  =  z  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
54alequcoms 1579 . . . 4  |-  ( A. z  z  =  x  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
6 ax10o 1696 . . . . . . 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 1696 . . . . . 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 1579 . . . 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 1602 . 2  |-  ( A. x  x  =  y  ->  A. x A. z  x  =  y )
13 ax-7 1444 . 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 1441
This theorem is referenced by:  hbaes  1704  hbnae  1705  dral1  1713  dral2  1715  drex2  1718  sbequ5  1754  aev  1772  hbsb4  1819  sbcom  1829  sbcom2  1916  exists1  2038  copsexg  3806  axextnd  7685  axrepnd  7688  axunnd  7690  axpowndlem3  7693  axpownd  7695  axregndlem1  7696  axregnd  7698  axacndlem1  7701  axacndlem2  7702  axacndlem3  7703  axacndlem4  7704  axacndlem5  7705  axacnd  7706  copsexgb  22808  a9e2eq  25635  a12stdy3  27481
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1442  ax-6 1443  ax-7 1444  ax-gen 1445  ax-8 1524  ax-11 1525  ax-17 1529  ax-12o 1562  ax-10 1576  ax-9 1582  ax-4 1589
This theorem depends on definitions:  df-bi 175  df-ex 1447
Copyright terms: Public domain