Theorem hbae-o

Description: All variables are effectively bound in an identical variable specifier. Version of hbae using ax-c11 . (Contributed by NM, 13-May-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	hbae-o	|- ( A. x x = y -> A. z A. x x = y )

Proof

Step	Hyp	Ref	Expression
1		ax-c5	|- ( A. x x = y -> x = y )
2		ax-c9	|- ( -. A. z z = x -> ( -. A. z z = y -> ( x = y -> A. z x = y ) ) )
3	1 2	syl7	|- ( -. A. z z = x -> ( -. A. z z = y -> ( A. x x = y -> A. z x = y ) ) )
4		ax-c11	|- ( A. x x = z -> ( A. x x = y -> A. z x = y ) )
5	4	aecoms-o	|- ( A. z z = x -> ( A. x x = y -> A. z x = y ) )
6		ax-c11	|- ( A. x x = y -> ( A. x x = y -> A. y x = y ) )
7	6	pm2.43i	|- ( A. x x = y -> A. y x = y )
8		ax-c11	|- ( A. y y = z -> ( A. y x = y -> A. z x = y ) )
9	7 8	syl5	|- ( A. y y = z -> ( A. x x = y -> A. z x = y ) )
10	9	aecoms-o	|- ( A. z z = y -> ( A. x x = y -> A. z x = y ) )
11	3 5 10	pm2.61ii	|- ( A. x x = y -> A. z x = y )
12	11	axc4i-o	|- ( A. x x = y -> A. x A. z x = y )
13		ax-11	|- ( A. x A. z x = y -> A. z A. x x = y )
14	12 13	syl	|- ( A. x x = y -> A. z A. x x = y )