Theorem wl-ax11-lem3 33364

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 2029	. 2 |- F/ x -. A. x x = y
2		wl-naev 33302	. . . . 5 |- ( -. A. x x = y -> -. A. u u = x )
3		nfa1 2028	. . . . . . 7 |- F/ u A. u u = y
4		nfna1 2029	. . . . . . 7 |- F/ u -. A. u u = x
5	3, 4	nfan 1828	. . . . . 6 |- F/ u ( A. u u = y /\ -. A. u u = x )
6		axc11n 2307	. . . . . . . . . . 11 |- ( A. x x = y -> A. y y = x )
7		wl-aetr 33317	. . . . . . . . . . 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 2312	. . . . . . . . 9 |- ( A. u u = y -> ( A. x x = y -> A. u u = x ) )
10	9	con3d 148	. . . . . . . 8 |- ( A. u u = y -> ( -. A. u u = x -> -. A. x x = y ) )
11	10	imdistani 726	. . . . . . 7 |- ( ( A. u u = y /\ -. A. u u = x ) -> ( A. u u = y /\ -. A. x x = y ) )
12		wl-ax11-lem2 33363	. . . . . . 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 2082	. . . . 5 |- ( ( A. u u = y /\ -. A. u u = x ) -> A. u A. x u = y )
15	2, 14	sylan2 491	. . . 4 |- ( ( A. u u = y /\ -. A. x x = y ) -> A. u A. x u = y )
16	15	expcom 451	. . 3 |- ( -. A. x x = y -> ( A. u u = y -> A. u A. x u = y ) )
17		ax-wl-11v 33361	. . 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	nf5d 2118	1 |- ( -. A. x x = y -> F/ x A. u u = y )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047  ax-13 2246  ax-wl-11v 33361

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by:  wl-ax11-lem4  33365  wl-ax11-lem6  33367