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

Theorem hbae 1583
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 1471 . . . . 5 |- (A.x x = y -> x = y)
2 ax-12 1441 . . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
31, 2syl7 62 . . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4 ax10o 1580 . . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
54alequcoms 1447 . . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6 ax10o 1580 . . . . . . 7 |- (A.x x = y -> (A.x x = y -> A.y x = y))
76pm2.43i 42 . . . . . 6 |- (A.x x = y -> A.y x = y)
8 ax10o 1580 . . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
97, 8syl5 27 . . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
109alequcoms 1447 . . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
113, 5, 10pm2.61ii 154 . . 3 |- (A.x x = y -> A.z x = y)
1211a5i 1484 . 2 |- (A.x x = y -> A.xA.z x = y)
13 ax-7 1353 . 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 1350
This theorem is referenced by:  hbaes 1584  hbnae 1585  dral1 1591  dral2 1592  drex2 1594  sbequ5 1629  aev 1647  hbsb4 1691  sbcom 1701  sbcom2 1787  a12stdy3 1826  exists1 1918  copsexg 3560  axextnd 6578  axrepnd 6581  axunndlem1 6582  axunnd 6583  axpowndlem3 6586  axpownd 6588  axregndlem1 6589  axregnd 6591  axacndlem1 6594  axacndlem2 6595  axacndlem3 6596  axacndlem4 6597  axacndlem5 6598  axacnd 6599  copsexgb 15597  a9e2eq 17739
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1351  ax-6 1352  ax-7 1353  ax-gen 1354  ax-8 1438  ax-10 1439  ax-11 1440  ax-12 1441  ax-17 1450  ax-9 1465  ax-4 1471
This theorem depends on definitions:  df-bi 175  df-ex 1356
Copyright terms: Public domain