Theorem wl-ax11-lem3

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

	Ref	Expression
Assertion	wl-ax11-lem3	|- ( -. A. x x = y -> F/ x A. u u = y )

Proof

Step	Hyp	Ref	Expression
1		nfna1	|- F/ x -. A. x x = y
2		naev	|- ( -. A. x x = y -> -. A. u u = x )
3		nfa1	|- F/ u A. u u = y
4		nfna1	|- F/ u -. A. u u = x
5	3 4	nfan	|- F/ u ( A. u u = y /\ -. A. u u = x )
6		axc11n	|- ( A. x x = y -> A. y y = x )
7		wl-aetr	|- ( A. y y = u -> ( A. y y = x -> A. u u = x ) )
8	6 7	syl5	|- ( A. y y = u -> ( A. x x = y -> A. u u = x ) )
9	8	aecoms	|- ( A. u u = y -> ( A. x x = y -> A. u u = x ) )
10	9	con3d	|- ( A. u u = y -> ( -. A. u u = x -> -. A. x x = y ) )
11	10	imdistani	|- ( ( A. u u = y /\ -. A. u u = x ) -> ( A. u u = y /\ -. A. x x = y ) )
12		wl-ax11-lem2	|- ( ( A. u u = y /\ -. A. x x = y ) -> A. x u = y )
13	11 12	syl	|- ( ( A. u u = y /\ -. A. u u = x ) -> A. x u = y )
14	5 13	alrimi	|- ( ( A. u u = y /\ -. A. u u = x ) -> A. u A. x u = y )
15	2 14	sylan2	|- ( ( A. u u = y /\ -. A. x x = y ) -> A. u A. x u = y )
16	15	expcom	|- ( -. A. x x = y -> ( A. u u = y -> A. u A. x u = y ) )
17		ax-wl-11v	|- ( A. u A. x u = y -> A. x A. u u = y )
18	16 17	syl6	|- ( -. A. x x = y -> ( A. u u = y -> A. x A. u u = y ) )
19	1 18	nf5d	|- ( -. A. x x = y -> F/ x A. u u = y )