Theorem hbae 1128

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 1104	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2		ax-4 951	. . . . 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-10 1103	. . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
5	4	alequcoms 1126	. . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6		ax-10 1103	. . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7		ax-10 1103	. . . . . . 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 1126	. . . 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 965	. 2 |- (A.x x = y -> A.xA.z x = y)
13		ax-7 954	. 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 950   = wceq 1099

This theorem is referenced by:  hbaes 1129  hbnae 1130  dral2 1138  drex2 1140  equvini 1151  sbequ5 1173  aev 1192  hbsb4 1232  sbcom 1242  a16g 1258  sbcom2 1316  a12stdy3 1351  exists1 1434  axextnd 4866  axrepnd 4869  axunndlem1 4870  axunnd 4871  axpowndlem3 4874  axpownd 4876  axregndlem1 4877  axregnd 4879  axacndlem1 4882  axacndlem2 4883  axacndlem3 4884  axacndlem4 4885  axacndlem5 4886  axacnd 4887

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain