Theorem wl-ax11-lem3 31875

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 1959	. 2 |- F/ x -. A. x x = y
2		wl-naev 31820	. . . . 5 |- ( -. A. x x = y -> -. A. u u = x )
3		nfa1 1953	. . . . . . 7 |- F/ u A. u u = y
4		nfna1 1959	. . . . . . 7 |- F/ u -. A. u u = x
5	3, 4	nfan 1985	. . . . . 6 |- F/ u ( A. u u = y /\ -. A. u u = x )
6		axc11n 2105	. . . . . . . . . . 11 |- ( A. x x = y -> A. y y = x )
7		wl-aetr 31821	. . . . . . . . . . 11 |- ( A. y y = u -> ( A. y y = x -> A. u u = x ) )
8	6, 7	syl5 34	. . . . . . . . . 10 |- ( A. y y = u -> ( A. x x = y -> A. u u = x ) )
9	8	aecoms 2108	. . . . . . . . 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 695	. . . . . . 7 |- ( ( A. u u = y /\ -. A. u u = x ) -> ( A. u u = y /\ -. A. x x = y ) )
12		wl-ax11-lem2 31874	. . . . . . 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 1929	. . . . 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 31872	. . 3 |- ( A. u A. x u = y -> A. x A. u u = y )
18	16, 17	syl6 35	. 2 |- ( -. A. x x = y -> ( A. u u = y -> A. x A. u u = y ) )
19	1, 18	nfd 1930	1 |- ( -. A. x x = y -> F/ x A. u u = y )

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-12 1906  ax-13 2054  ax-wl-11v 31872

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-nf 1665

This theorem is referenced by:  wl-ax11-lem4  31876  wl-ax11-lem6  31878