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

Theorem hbae 1598
Description: All variables are effectively bound in an identical variable specifier.
Assertion
Ref Expression
hbae |- (A.x x = y -> A.zA.x x = y)

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1486 . . . . 5 |- (A.x x = y -> x = y)
2 ax-12 1456 . . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
31, 2syl7 62 . . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4 ax10o 1595 . . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
54alequcoms 1462 . . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6 ax10o 1595 . . . . . . 7 |- (A.x x = y -> (A.x x = y -> A.y x = y))
76pm2.43i 42 . . . . . 6 |- (A.x x = y -> A.y x = y)
8 ax10o 1595 . . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
97, 8syl5 27 . . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
109alequcoms 1462 . . . 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 1499 . 2 |- (A.x x = y -> A.xA.z x = y)
13 ax-7 1369 . 2 |- (A.xA.z x = y -> A.zA.x x = y)
1412, 13syl 14 1 |- (A.x x = y -> A.zA.x x = y)
Colors of variables: wff set class
Syntax hints:  -. wn 3   -> wi 4  A.wal 1366
This theorem is referenced by:  hbaes 1599  hbnae 1600  dral1 1606  dral2 1607  drex2 1609  sbequ5 1644  aev 1662  hbsb4 1706  sbcom 1716  sbcom2 1802  a12stdy3 1841  exists1 1933  copsexg 3569  axextnd 6586  axrepnd 6589  axunndlem1 6590  axunnd 6591  axpowndlem3 6594  axpownd 6596  axregndlem1 6597  axregnd 6599  axacndlem1 6602  axacndlem2 6603  axacndlem3 6604  axacndlem4 6605  axacndlem5 6606  axacnd 6607  copsexgb 15457  a9e2eq 17599
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1367  ax-6 1368  ax-7 1369  ax-gen 1370  ax-8 1453  ax-10 1454  ax-11 1455  ax-12 1456  ax-17 1465  ax-9 1480  ax-4 1486
This theorem depends on definitions:  df-bi 185  df-ex 1372
Copyright terms: Public domain