Description: Elimination of substitution. Also see sbel2x . (Contributed by NM, 5-Aug-1993) Avoid ax-13 . (Revised by Wolf Lammen, 6-Aug-2023) Avoid ax-10 . (Revised by Gino Giotto, 20-Aug-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sbelx | |- ( ph <-> E. x ( x = y /\ [ x / y ] ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sbequ12r | |- ( x = y -> ( [ x / y ] ph <-> ph ) ) |
|
| 2 | 1 | equsexvw | |- ( E. x ( x = y /\ [ x / y ] ph ) <-> ph ) |
| 3 | 2 | bicomi | |- ( ph <-> E. x ( x = y /\ [ x / y ] ph ) ) |