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

Theorem hbae 1606
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 1494 . . . . 5 |- (A.x x = y -> x = y)
2 ax-12 1464 . . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
31, 2syl7 65 . . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4 ax10o 1603 . . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
54alequcoms 1470 . . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6 ax10o 1603 . . . . . . 7 |- (A.x x = y -> (A.x x = y -> A.y x = y))
76pm2.43i 45 . . . . . 6 |- (A.x x = y -> A.y x = y)
8 ax10o 1603 . . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
97, 8syl5 29 . . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
109alequcoms 1470 . . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
113, 5, 10pm2.61ii 160 . . 3 |- (A.x x = y -> A.z x = y)
1211a5i 1507 . 2 |- (A.x x = y -> A.xA.z x = y)
13 ax-7 1378 . 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 1375
This theorem is referenced by:  hbaes 1607  hbnae 1608  dral1 1614  dral2 1615  drex2 1617  sbequ5 1652  aev 1670  hbsb4 1714  sbcom 1724  sbcom2 1810  a12stdy3 1849  exists1 1941  axextnd 6596  axrepnd 6599  axunndlem1 6600  axunnd 6601  axpowndlem3 6604  axpownd 6606  axregndlem1 6607  axregnd 6609  axacndlem1 6612  axacndlem2 6613  axacndlem3 6614  axacndlem4 6615  axacndlem5 6616  axacnd 6617  copsexgb 15208  a9e2eq 17393
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1376  ax-6 1377  ax-7 1378  ax-gen 1379  ax-8 1461  ax-10 1462  ax-11 1463  ax-12 1464  ax-17 1473  ax-9 1488  ax-4 1494
This theorem depends on definitions:  df-bi 190  df-ex 1381
Copyright terms: Public domain