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