Description: An equivalence for class substitution in the spirit of df-clab . Note that x and A don't have to be distinct. (Contributed by NM, 18-Nov-2008) (Revised by Mario Carneiro, 13-Oct-2016)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbc7 | |- ( [. A / x ]. ph <-> E. y ( y = A /\ [. y / x ]. ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbccow | |- ( [. A / y ]. [. y / x ]. ph <-> [. A / x ]. ph ) |
|
| 2 | sbc5 | |- ( [. A / y ]. [. y / x ]. ph <-> E. y ( y = A /\ [. y / x ]. ph ) ) |
|
| 3 | 1 2 | bitr3i | |- ( [. A / x ]. ph <-> E. y ( y = A /\ [. y / x ]. ph ) ) |