Description: Substitution for the first argument of the non-logical predicate in an atomic formula. See elsb2 for substitution for the second argument. (Contributed by NM, 7-Nov-2006) (Proof shortened by Andrew Salmon, 14-Jun-2011) Reduce axiom usage. (Revised by Wolf Lammen, 24-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elsb1 | |- ( [ y / x ] x e. z <-> y e. z ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elequ1 | |- ( x = w -> ( x e. z <-> w e. z ) ) |
|
| 2 | elequ1 | |- ( w = y -> ( w e. z <-> y e. z ) ) |
|
| 3 | 1 2 | sbievw2 | |- ( [ y / x ] x e. z <-> y e. z ) |