Theorem wl-ax11-lem3 31917

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 1985	. 2 |- F/ x -. A. x x = y
2		wl-naev 31862	. . . . 5 |- ( -. A. x x = y -> -. A. u u = x )
3		nfa1 1979	. . . . . . 7 |- F/ u A. u u = y
4		nfna1 1985	. . . . . . 7 |- F/ u -. A. u u = x
5	3, 4	nfan 2011	. . . . . 6 |- F/ u ( A. u u = y /\ -. A. u u = x )
6		axc11n 2143	. . . . . . . . . . 11 |- ( A. x x = y -> A. y y = x )
7		wl-aetr 31863	. . . . . . . . . . 11 |- ( A. y y = u -> ( A. y y = x -> A. u u = x ) )
8	6, 7	syl5 33	. . . . . . . . . 10 |- ( A. y y = u -> ( A. x x = y -> A. u u = x ) )
9	8	aecoms 2146	. . . . . . . . 9 |- ( A. u u = y -> ( A. x x = y -> A. u u = x ) )
10	9	con3d 139	. . . . . . . 8 |- ( A. u u = y -> ( -. A. u u = x -> -. A. x x = y ) )
11	10	imdistani 696	. . . . . . 7 |- ( ( A. u u = y /\ -. A. u u = x ) -> ( A. u u = y /\ -. A. x x = y ) )
12		wl-ax11-lem2 31916	. . . . . . 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 1955	. . . . 5 |- ( ( A. u u = y /\ -. A. u u = x ) -> A. u A. x u = y )
15	2, 14	sylan2 477	. . . 4 |- ( ( A. u u = y /\ -. A. x x = y ) -> A. u A. x u = y )
16	15	expcom 437	. . 3 |- ( -. A. x x = y -> ( A. u u = y -> A. u A. x u = y ) )
17		ax-wl-11v 31914	. . 3 |- ( A. u A. x u = y -> A. x A. u u = y )
18	16, 17	syl6 34	. 2 |- ( -. A. x x = y -> ( A. u u = y -> A. x A. u u = y ) )
19	1, 18	nfd 1956	1 |- ( -. A. x x = y -> F/ x A. u u = y )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 371   A.wal 1442   F/wnf 1667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-12 1933  ax-13 2091  ax-wl-11v 31914

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668

This theorem is referenced by:  wl-ax11-lem4  31918  wl-ax11-lem6  31920