Theorem wl-ax11-lem3 31379

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

Assertion

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

Distinct variable group:   x, u

Proof of Theorem wl-ax11-lem3

Step	Hyp	Ref	Expression
1		nfna1 1931	. 2 |- F/ x -. A. x x = y
2		wl-naev 31334	. . . . 5 |- ( -. A. x x = y -> -. A. u u = x )
3		nfa1 1925	. . . . . . 7 |- F/ u A. u u = y
4		nfna1 1931	. . . . . . 7 |- F/ u -. A. u u = x
5	3, 4	nfan 1956	. . . . . 6 |- F/ u ( A. u u = y /\ -. A. u u = x )
6		axc11n 2075	. . . . . . . . . . 11 |- ( A. x x = y -> A. y y = x )
7		wl-aetr 31335	. . . . . . . . . . 11 |- ( A. y y = u -> ( A. y y = x -> A. u u = x ) )
8	6, 7	syl5 30	. . . . . . . . . 10 |- ( A. y y = u -> ( A. x x = y -> A. u u = x ) )
9	8	aecoms 2078	. . . . . . . . 9 |- ( A. u u = y -> ( A. x x = y -> A. u u = x ) )
10	9	con3d 133	. . . . . . . 8 |- ( A. u u = y -> ( -. A. u u = x -> -. A. x x = y ) )
11	10	imdistani 688	. . . . . . 7 |- ( ( A. u u = y /\ -. A. u u = x ) -> ( A. u u = y /\ -. A. x x = y ) )
12		wl-ax11-lem2 31378	. . . . . . 7 |- ( ( A. u u = y /\ -. A. x x = y ) -> A. x u = y )
13	11, 12	syl 17	. . . . . 6 |- ( ( A. u u = y /\ -. A. u u = x ) -> A. x u = y )
14	5, 13	alrimi 1901	. . . . 5 |- ( ( A. u u = y /\ -. A. u u = x ) -> A. u A. x u = y )
15	2, 14	sylan2 472	. . . 4 |- ( ( A. u u = y /\ -. A. x x = y ) -> A. u A. x u = y )
16	15	expcom 433	. . 3 |- ( -. A. x x = y -> ( A. u u = y -> A. u A. x u = y ) )
17		ax-wl-11v 31376	. . 3 |- ( A. u A. x u = y -> A. x A. u u = y )
18	16, 17	syl6 31	. 2 |- ( -. A. x x = y -> ( A. u u = y -> A. x A. u u = y ) )
19	1, 18	nfd 1902	1 |- ( -. A. x x = y -> F/ x A. u u = y )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 367   A.wal 1403   F/wnf 1637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-12 1878  ax-13 2026  ax-wl-11v 31376

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-nf 1638

This theorem is referenced by:  wl-ax11-lem4  31380  wl-ax11-lem6  31382