Theorem hbae 1560

Description: All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)

Assertion

Ref	Expression
hbae	|- (A.x x = y -> A.zA.x x = y)

Proof of Theorem hbae

Step	Hyp	Ref	Expression
1		ax12or 1365	. . . 4 |- (A.z z = x \/ (A.z z = y \/ A.z(x = y -> A.z x = y)))
2		ax10o 1557	. . . . . 6 |- (A.x x = z -> (A.x x = y -> A.z x = y))
3	2	alequcoms 1371	. . . . 5 |- (A.z z = x -> (A.x x = y -> A.z x = y))
4		ax10o 1557	. . . . . . . . 9 |- (A.x x = y -> (A.x x = y -> A.y x = y))
5	4	pm2.43i 41	. . . . . . . 8 |- (A.x x = y -> A.y x = y)
6		ax10o 1557	. . . . . . . 8 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7	5, 6	syl5 26	. . . . . . 7 |- (A.y y = z -> (A.x x = y -> A.z x = y))
8	7	alequcoms 1371	. . . . . 6 |- (A.z z = y -> (A.x x = y -> A.z x = y))
9		ax-4 1362	. . . . . . . 8 |- (A.x x = y -> x = y)
10	9	imim1i 52	. . . . . . 7 |- ((x = y -> A.z x = y) -> (A.x x = y -> A.z x = y))
11	10	sps 1393	. . . . . 6 |- (A.z(x = y -> A.z x = y) -> (A.x x = y -> A.z x = y))
12	8, 11	jaoi 618	. . . . 5 |- ((A.z z = y \/ A.z(x = y -> A.z x = y)) -> (A.x x = y -> A.z x = y))
13	3, 12	jaoi 618	. . . 4 |- ((A.z z = x \/ (A.z z = y \/ A.z(x = y -> A.z x = y))) -> (A.x x = y -> A.z x = y))
14	1, 13	ax-mp 7	. . 3 |- (A.x x = y -> A.z x = y)
15	14	a5i 1398	. 2 |- (A.x x = y -> A.xA.z x = y)
16		ax-7 1296	. 2 |- (A.xA.z x = y -> A.zA.x x = y)
17	15, 16	syl 13	1 |- (A.x x = y -> A.zA.x x = y)

Syntax hints:   -> wi 4   \/ wo 611  A.wal 1294   = wceq 1353

This theorem is referenced by:  nfae  1561  hbaes  1562  hbnae  1563  dral1  1571  dral2  1572  drex2  1573  drex1  1632  aev  1646  sbcomxyyz  1795  exists1  1940

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-io 612  ax-5 1295  ax-7 1296  ax-gen 1297  ax-ie2 1343  ax-8 1357  ax-10 1358  ax-11 1359  ax-i12 1360  ax-4 1362  ax-17 1381  ax-i9 1385  ax-ial 1390

This theorem depends on definitions:  df-bi 108