Theorem eq5 824

Description: All variables are effectively bound in an identical variable specifier.

Assertion

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

Proof of Theorem eq5

Step	Hyp	Ref	Expression
1		ax-12 802	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
2		ax-4 673	. . . . 5 |- (A.x x = y -> x = y)
3	1, 2	syl7 24	. . . 4 |- (-. A.z z = x -> (-. A.z z = y -> (A.x x = y -> A.z x = y)))
4		ax-10 800	. . . . 5 |- (A.x x = z -> (A.x x = y -> A.z x = y))
5	4	eq4s 822	. . . 4 |- (A.z z = x -> (A.x x = y -> A.z x = y))
6		ax-10 800	. . . . . 6 |- (A.y y = z -> (A.y x = y -> A.z x = y))
7		ax-10 800	. . . . . . 7 |- (A.x x = y -> (A.x x = y -> A.y x = y))
8	7	pm2.43i 58	. . . . . 6 |- (A.x x = y -> A.y x = y)
9	6, 8	syl5 22	. . . . 5 |- (A.y y = z -> (A.x x = y -> A.z x = y))
10	9	eq4s 822	. . . 4 |- (A.z z = y -> (A.x x = y -> A.z x = y))
11	3, 5, 10	pm2.61ii 113	. . 3 |- (A.x x = y -> A.z x = y)
12	11	a5i 687	. 2 |- (A.x x = y -> A.xA.z x = y)
13		ax-7 676	. 2 |- (A.xA.z x = y -> A.zA.x x = y)
14	12, 13	syl 12	1 |- (A.x x = y -> A.zA.x x = y)

Syntax hints:  -. wn 1   -> wi 2  A.wal 672   = weq 797

This theorem is referenced by:  eq5s 825  eq6 826  sbequ5 898  hbsb4 905  sbcom 916  a16g 933  sbcom2 992  exists1 1072  rgen2 1248  ralcom2 1314  alexeq 1409  axrepnd 3740  axunndlem1 3741  axunnd 3742  axpownd 3747  axregndlem1 3748  axacndlem1 3753  axacndlem2 3754  axacndlem3 3755  axacndlem4 3756  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org