Description: Substitution applied to an atomic wff (class version of elsb3 ). (Contributed by Rodolfo Medina, 28-Apr-2010) (Proof shortened by Andrew Salmon, 14-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | clelsb3 | |- ( [ y / x ] x e. A <-> y e. A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1w | |- ( x = w -> ( x e. A <-> w e. A ) ) |
|
| 2 | eleq1w | |- ( w = y -> ( w e. A <-> y e. A ) ) |
|
| 3 | 1 2 | sbievw2 | |- ( [ y / x ] x e. A <-> y e. A ) |