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

Theorem hbae 1737
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 1626 . . . . 5 |- (A.x x = y -> x = y)
2 ax-12 1599 . . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
31, 2syl7 68 . . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4 ax10o 1734 . . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
54alequcoms 1605 . . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6 ax10o 1734 . . . . . . 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 1734 . . . . . 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 1605 . . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
113, 5, 10pm2.61ii 177 . . 3 |- (A.x x = y -> A.z x = y)
1211a5i 1639 . 2 |- (A.x x = y -> A.xA.z x = y)
13 ax-7 1518 . 2 |- (A.xA.z x = y -> A.zA.x x = y)
1412, 13syl 13 1 |- (A.x x = y -> A.zA.x x = y)
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3  A.wal 1515
This theorem is referenced by:  hbaes 1738  hbnae 1739  dral1 1745  dral2 1746  drex2 1748  sbequ5 1783  aev 1801  hbsb4 1845  sbcom 1855  sbcom2 1941  a12stdy3 1980  exists1 2072  a9e2eq 6325  axextnd 6804  axrepnd 6807  axunndlem1 6808  axunnd 6809  axpowndlem3 6812  axpownd 6814  axregndlem1 6815  axregnd 6817  axacndlem1 6820  axacndlem2 6821  axacndlem3 6822  axacndlem4 6823  axacndlem5 6824  axacnd 6825  coprsexg 14783
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1516  ax-6 1517  ax-7 1518  ax-gen 1519  ax-8 1596  ax-10 1597  ax-11 1598  ax-12 1599  ax-17 1608  ax-9 1620  ax-4 1626
This theorem depends on definitions:  df-bi 210  df-ex 1521
Copyright terms: Public domain