Theorem hbae 1603

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 1400	. . . 4 |- (A.z z = x \/ (A.z z = y \/ A.z(x = y -> A.z x = y)))
2		ax10o 1600	. . . . . 6 |- (A.x x = z -> (A.x x = y -> A.z x = y))
3	2	alequcoms 1406	. . . . 5 |- (A.z z = x -> (A.x x = y -> A.z x = y))
4		ax10o 1600	. . . . . . . . 9 |- (A.x x = y -> (A.x x = y -> A.y x = y))
5	4	pm2.43i 43	. . . . . . . 8 |- (A.x x = y -> A.y x = y)
6		ax10o 1600	. . . . . . . 8 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7	5, 6	syl5 28	. . . . . . 7 |- (A.y y = z -> (A.x x = y -> A.z x = y))
8	7	alequcoms 1406	. . . . . 6 |- (A.z z = y -> (A.x x = y -> A.z x = y))
9		ax-4 1397	. . . . . . . 8 |- (A.x x = y -> x = y)
10	9	imim1i 54	. . . . . . 7 |- ((x = y -> A.z x = y) -> (A.x x = y -> A.z x = y))
11	10	sps 1427	. . . . . 6 |- (A.z(x = y -> A.z x = y) -> (A.x x = y -> A.z x = y))
12	8, 11	jaoi 635	. . . . 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 635	. . . 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 1432	. 2 |- (A.x x = y -> A.xA.z x = y)
16		ax-7 1334	. 2 |- (A.xA.z x = y -> A.zA.x x = y)
17	15, 16	syl 14	1 |- (A.x x = y -> A.zA.x x = y)

Syntax hints:   -> wi 4   \/ wo 628  A.wal 1240   = wceq 1242

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  nfae  1604  hbaes  1605  hbnae  1606  dral1  1615  dral2  1616  drex2  1617  drex1  1676  aev  1690  sbcomxyyz  1843  exists1  1993