Theorem hbae 1145

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 968	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2		ax-4 973	. . . . 5 |- (A.x x = y -> x = y)
3	1, 2	syl7 23	. . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4		ax-10o 1140	. . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
5	4	alequcoms 1143	. . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6		ax-10o 1140	. . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7		ax-10o 1140	. . . . . . 7 |- (A.x x = y -> (A.x x = y -> A.y x = y))
8	7	pm2.43i 64	. . . . . 6 |- (A.x x = y -> A.y x = y)
9	6, 8	syl5 21	. . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
10	9	alequcoms 1143	. . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
11	3, 5, 10	pm2.61ii 130	. . 3 |- (A.x x = y -> A.z x = y)
12	11	a5i 989	. 2 |- (A.x x = y -> A.xA.z x = y)
13		ax-7 962	. 2 |- (A.xA.z x = y -> A.zA.x x = y)
14	12, 13	syl 10	1 |- (A.x x = y -> A.zA.x x = y)

Syntax hints:  -. wn 2   -> wi 3  A.wal 954   = wceq 956

This theorem is referenced by:  hbaes 1146  hbnae 1147  dral1 1154  dral2 1155  drex2 1157  equvini 1168  sbequ5 1190  aev 1208  hbsb4 1248  sbcom 1258  a16g 1276  sbcom2 1334  a12stdy3 1374  exists1 1457  axextnd 4943  axrepnd 4946  axunndlem1 4947  axunnd 4948  axpowndlem3 4951  axpownd 4953  axregndlem1 4954  axregnd 4956  axacndlem1 4959  axacndlem2 4960  axacndlem3 4961  axacndlem4 4962  axacndlem5 4963  axacnd 4964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-10 966  ax-12 968  ax-4 973  ax-5o 975  ax-10o 1140

Copyright terms: Public domain