Theorem wl-ax11-lem8

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

	Ref	Expression
Assertion	wl-ax11-lem8	|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. u A. x [ u / y ] ph <-> A. y A. x ph ) )

Proof

Step	Hyp	Ref	Expression
1		axc11n	|- ( A. y y = x -> A. x x = y )
2	1	con3i	|- ( -. A. x x = y -> -. A. y y = x )
3		wl-ax11-lem1	|- ( A. u u = y -> ( A. u u = x <-> A. y y = x ) )
4	3	notbid	|- ( A. u u = y -> ( -. A. u u = x <-> -. A. y y = x ) )
5	4	anbi1d	|- ( A. u u = y -> ( ( -. A. u u = x /\ A. u A. x [ u / y ] ph ) <-> ( -. A. y y = x /\ A. u A. x [ u / y ] ph ) ) )
6	4	anbi1d	|- ( A. u u = y -> ( ( -. A. u u = x /\ A. x [ u / y ] ph ) <-> ( -. A. y y = x /\ A. x [ u / y ] ph ) ) )
7		axc11n	|- ( A. x x = y -> A. y y = x )
8	7	con3i	|- ( -. A. y y = x -> -. A. x x = y )
9		wl-ax11-lem4	|- F/ x ( A. u u = y /\ -. A. x x = y )
10		sbequ12	|- ( y = u -> ( ph <-> [ u / y ] ph ) )
11	10	equcoms	|- ( u = y -> ( ph <-> [ u / y ] ph ) )
12	11	sps	|- ( A. u u = y -> ( ph <-> [ u / y ] ph ) )
13	12	adantr	|- ( ( A. u u = y /\ -. A. x x = y ) -> ( ph <-> [ u / y ] ph ) )
14	9 13	albid	|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. x ph <-> A. x [ u / y ] ph ) )
15	14	ex	|- ( A. u u = y -> ( -. A. x x = y -> ( A. x ph <-> A. x [ u / y ] ph ) ) )
16	8 15	syl5	|- ( A. u u = y -> ( -. A. y y = x -> ( A. x ph <-> A. x [ u / y ] ph ) ) )
17	16	pm5.32d	|- ( A. u u = y -> ( ( -. A. y y = x /\ A. x ph ) <-> ( -. A. y y = x /\ A. x [ u / y ] ph ) ) )
18	6 17	bitr4d	|- ( A. u u = y -> ( ( -. A. u u = x /\ A. x [ u / y ] ph ) <-> ( -. A. y y = x /\ A. x ph ) ) )
19	18	dral1	|- ( A. u u = y -> ( A. u ( -. A. u u = x /\ A. x [ u / y ] ph ) <-> A. y ( -. A. y y = x /\ A. x ph ) ) )
20		wl-ax11-lem7	|- ( A. u ( -. A. u u = x /\ A. x [ u / y ] ph ) <-> ( -. A. u u = x /\ A. u A. x [ u / y ] ph ) )
21		wl-ax11-lem7	|- ( A. y ( -. A. y y = x /\ A. x ph ) <-> ( -. A. y y = x /\ A. y A. x ph ) )
22	19 20 21	3bitr3g	|- ( A. u u = y -> ( ( -. A. u u = x /\ A. u A. x [ u / y ] ph ) <-> ( -. A. y y = x /\ A. y A. x ph ) ) )
23	5 22	bitr3d	|- ( A. u u = y -> ( ( -. A. y y = x /\ A. u A. x [ u / y ] ph ) <-> ( -. A. y y = x /\ A. y A. x ph ) ) )
24		pm5.32	|- ( ( -. A. y y = x -> ( A. u A. x [ u / y ] ph <-> A. y A. x ph ) ) <-> ( ( -. A. y y = x /\ A. u A. x [ u / y ] ph ) <-> ( -. A. y y = x /\ A. y A. x ph ) ) )
25	23 24	sylibr	|- ( A. u u = y -> ( -. A. y y = x -> ( A. u A. x [ u / y ] ph <-> A. y A. x ph ) ) )
26	25	imp	|- ( ( A. u u = y /\ -. A. y y = x ) -> ( A. u A. x [ u / y ] ph <-> A. y A. x ph ) )
27	2 26	sylan2	|- ( ( A. u u = y /\ -. A. x x = y ) -> ( A. u A. x [ u / y ] ph <-> A. y A. x ph ) )