Description: A lemma for the definiens of df-sb . An instance of sp proved without it. Note: it has a common subproof with sbjust . (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ssblem1 | |- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> ( y = t -> A. x ( x = y -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equequ1 | |- ( y = z -> ( y = t <-> z = t ) ) |
|
| 2 | equequ2 | |- ( y = z -> ( x = y <-> x = z ) ) |
|
| 3 | 2 | imbi1d | |- ( y = z -> ( ( x = y -> ph ) <-> ( x = z -> ph ) ) ) |
| 4 | 3 | albidv | |- ( y = z -> ( A. x ( x = y -> ph ) <-> A. x ( x = z -> ph ) ) ) |
| 5 | 1 4 | imbi12d | |- ( y = z -> ( ( y = t -> A. x ( x = y -> ph ) ) <-> ( z = t -> A. x ( x = z -> ph ) ) ) ) |
| 6 | 5 | spw | |- ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> ( y = t -> A. x ( x = y -> ph ) ) ) |