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

Step	Hyp	Ref	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)
3	1, 2	syl7 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))
5	4	alequcoms 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))
8	7	pm2.43i 78	. . . . . 6 |- (A.x x = y -> A.y x = y)
9	6, 8	syl5 20	. . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
10	9	alequcoms 1503	. . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
11	3, 5, 10	pm2.61ii 144	. . 3 |- (A.x x = y -> A.z x = y)
12	11	a5i 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)
14	12, 13	syl 12	1 |- (A.x x = y -> A.zA.x x = y)

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