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

Theorem hbae 1605
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 1602 . . . . 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 1602 . . . . . . 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 1602 . . . . . 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 1606  hbnae 1607  dral1 1613  dral2 1614  drex2 1616  sbequ5 1651  aev 1669  hbsb4 1713  sbcom 1723  sbcom2 1809  a12stdy3 1848  exists1 1940  axextnd 6563  axrepnd 6566  axunndlem1 6567  axunnd 6568  axpowndlem3 6571  axpownd 6573  axregndlem1 6574  axregnd 6576  axacndlem1 6579  axacndlem2 6580  axacndlem3 6581  axacndlem4 6582  axacndlem5 6583  axacnd 6584  copsexgb 15106  a9e2eq 17291
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