Theorem wl-sbcom2d-lem2

Description: Lemma used to prove wl-sbcom2d . (Contributed by Wolf Lammen, 10-Aug-2019) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( -. A. y y = x -> -. A. y y = x )
2		naev	|- ( -. A. y y = x -> -. A. y y = v )
3		naev	|- ( -. A. y y = x -> -. A. y y = u )
4		naev	|- ( -. A. y y = x -> -. A. x x = u )
5	1 2 3 4	wl-2sb6d	|- ( -. A. y y = x -> ( [ u / x ] [ v / y ] ph <-> A. x A. y ( ( x = u /\ y = v ) -> ph ) ) )