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

Theorem hbae 1707
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 1594 . . . . 5  |-  ( A. x  x  =  y  ->  x  =  y )
2 ax-12o 1567 . . . . 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 1701 . . . . 5  |-  ( A. x  x  =  z  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
54alequcoms 1584 . . . 4  |-  ( A. z  z  =  x  ->  ( A. x  x  =  y  ->  A. z  x  =  y )
)
6 ax10o 1701 . . . . . . 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 1701 . . . . . 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 1584 . . . 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 1607 . 2  |-  ( A. x  x  =  y  ->  A. x A. z  x  =  y )
13 ax-7 1448 . 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 1445
This theorem is referenced by:  hbaes  1709  hbnae  1710  dral1  1718  dral2  1720  drex2  1723  sbequ5  1759  aev  1777  hbsb4  1824  sbcom  1834  sbcom2  1921  exists1  2043  copsexg  3816  axextnd  7695  axrepnd  7698  axunnd  7700  axpowndlem3  7703  axpownd  7705  axregndlem1  7706  axregnd  7708  axacndlem1  7711  axacndlem2  7712  axacndlem3  7713  axacndlem4  7714  axacndlem5  7715  axacnd  7716  copsexgb  22831  a9e2eq  25690  a12stdy3  27533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1528  ax-11 1529  ax-17 1533  ax-12o 1567  ax-10 1581  ax-9 1587  ax-4 1594
This theorem depends on definitions:  df-bi 175  df-ex 1451
  Copyright terms: Public domain W3C validator