Theorem hbae 1141

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 965	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2		ax-4 970	. . . . 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 1136	. . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
5	4	alequcoms 1139	. . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6		ax-10o 1136	. . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7		ax-10o 1136	. . . . . . 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 1139	. . . 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 986	. 2 |- (A.x x = y -> A.xA.z x = y)
13		ax-7 959	. 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 951   = wceq 953

This theorem is referenced by:  hbaes 1142  hbnae 1143  dral1 1150  dral2 1151  drex2 1153  equvini 1164  sbequ5 1186  aev 1204  hbsb4 1243  sbcom 1253  a16g 1271  sbcom2 1329  a12stdy3 1367  exists1 1450  axextnd 4915  axrepnd 4918  axunndlem1 4919  axunnd 4920  axpowndlem3 4923  axpownd 4925  axregndlem1 4926  axregnd 4928  axacndlem1 4931  axacndlem2 4932  axacndlem3 4933  axacndlem4 4934  axacndlem5 4935  axacnd 4936

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-10 963  ax-12 965  ax-4 970  ax-5o 972  ax-10o 1136

Copyright terms: Public domain