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 6561  axrepnd 6564  axunndlem1 6565  axunnd 6566  axpowndlem3 6569  axpownd 6571  axregndlem1 6572  axregnd 6574  axacndlem1 6577  axacndlem2 6578  axacndlem3 6579  axacndlem4 6580  axacndlem5 6581  axacnd 6582  copsexgb 14997  a9e2eq 17189
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