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 6557  axrepnd 6560  axunndlem1 6561  axunnd 6562  axpowndlem3 6565  axpownd 6567  axregndlem1 6568  axregnd 6570  axacndlem1 6573  axacndlem2 6574  axacndlem3 6575  axacndlem4 6576  axacndlem5 6577  axacnd 6578  copsexgb 14807  a9e2eq 17002
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