Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993) (Revised by Mario Carneiro, 12-Oct-2016) (Proof shortened by SN, 2-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbc5 | |- ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-sbc | |- ( [. A / x ]. ph <-> A e. { x | ph } ) |
|
| 2 | clelab | |- ( A e. { x | ph } <-> E. x ( x = A /\ ph ) ) |
|
| 3 | 1 2 | bitri | |- ( [. A / x ]. ph <-> E. x ( x = A /\ ph ) ) |