Theorem wl-ax11-lem4

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

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

Proof

Step	Hyp	Ref	Expression
1		ancom	|- ( ( A. u u = y /\ -. A. x x = y ) <-> ( -. A. x x = y /\ A. u u = y ) )
2		nfna1	|- F/ x -. A. x x = y
3		wl-ax11-lem3	|- ( -. A. x x = y -> F/ x A. u u = y )
4	2 3	nfan1	|- F/ x ( -. A. x x = y /\ A. u u = y )
5	1 4	nfxfr	|- F/ x ( A. u u = y /\ -. A. x x = y )