Description: Substitution for the second argument of the membership predicate in an atomic formula (class version of elsb2 ). (Contributed by Jim Kingdon, 22-Nov-2018) Reduce dependencies on axioms. (Revised by Wolf Lammen, 24-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | clelsb2 | |- ( [ y / x ] A e. x <-> A e. y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq2w | |- ( x = z -> ( A e. x <-> A e. z ) ) |
|
| 2 | eleq2w | |- ( z = y -> ( A e. z <-> A e. y ) ) |
|
| 3 | 1 2 | sbievw2 | |- ( [ y / x ] A e. x <-> A e. y ) |