Description: In the case of stdpc4 , rename-sb is derivable from fewer axioms than dfsb . The essential proof step is presented in this lemma. Based on a proof of BJ, 22-Dec-2020. (Contributed by Wolf Lammen, 4-Jun-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | stdpc4lem | |- ( A. x ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ala1 | |- ( A. x ph -> A. x ( x = y -> ph ) ) |
|
| 2 | 1 | a1d | |- ( A. x ph -> ( y = t -> A. x ( x = y -> ph ) ) ) |
| 3 | 2 | alrimiv | |- ( A. x ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) ) |