Theorem hbae 1178

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 1000	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2		ax-4 1005	. . . . 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 1173	. . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
5	4	alequcoms 1176	. . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6		ax-10o 1173	. . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7		ax-10o 1173	. . . . . . 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 1176	. . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
11	3, 5, 10	pm2.61ii 128	. . 3 |- (A.x x = y -> A.z x = y)
12	11	a5i 1021	. 2 |- (A.x x = y -> A.xA.z x = y)
13		ax-7 994	. 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 986   = wceq 988

This theorem is referenced by:  hbaes 1179  hbnae 1180  dral1 1187  dral2 1188  drex2 1190  equvini 1201  sbequ5 1223  aev 1241  hbsb4 1281  sbcom 1291  a16g 1309  sbcom2 1367  a12stdy3 1407  exists1 1492  axextnd 5032  axrepnd 5035  axunndlem1 5036  axunnd 5037  axpowndlem3 5040  axpownd 5042  axregndlem1 5043  axregnd 5045  axacndlem1 5048  axacndlem2 5049  axacndlem3 5050  axacndlem4 5051  axacndlem5 5052  axacnd 5053

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-10 998  ax-12 1000  ax-4 1005  ax-5o 1007  ax-10o 1173

Copyright terms: Public domain