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

Theorem hbae 1505
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-12 1310 . . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2 ax-4 1319 . . . . 5 |- (A.x x = y -> x = y)
31, 2syl7 26 . . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4 ax-10o 1500 . . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
54alequcoms 1503 . . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6 ax-10o 1500 . . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7 ax-10o 1500 . . . . . . 7 |- (A.x x = y -> (A.x x = y -> A.y x = y))
87pm2.43i 78 . . . . . 6 |- (A.x x = y -> A.y x = y)
96, 8syl5 20 . . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
109alequcoms 1503 . . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
113, 5, 10pm2.61ii 144 . . 3 |- (A.x x = y -> A.z x = y)
1211a5i 1335 . 2 |- (A.x x = y -> A.xA.z x = y)
13 ax-7 1304 . 2 |- (A.xA.z x = y -> A.zA.x x = y)
1412, 13syl 12 1 |- (A.x x = y -> A.zA.x x = y)
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3  A.wal 1296   = wceq 1298
This theorem is referenced by:  hbaes 1506  hbnae 1507  dral1 1515  dral2 1516  drex2 1518  equviniOLD 1532  sbequ5 1557  aev 1577  aevOLD 1578  hbsb4 1620  sbcom 1632  a16gOLD 1654  sbcom2 1724  a12stdy3 1765  exists1 1862  axextnd 6095  axrepnd 6098  axunndlem1 6099  axunnd 6100  axpowndlem3 6103  axpownd 6105  axregndlem1 6106  axregnd 6108  axacndlem1 6111  axacndlem2 6112  axacndlem3 6113  axacndlem4 6114  axacndlem5 6115  axacnd 6116
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-10o 1500
Copyright terms: Public domain