Metamath Proof Explorer


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 ) ) )