Theorem elsb2

Substitution for the second argument of the non-logical predicate in an atomic formula. See elsb1 for substitution for the first argument. (Contributed by Rodolfo Medina, 3-Apr-2010.) (Proof shortened by Andrew Salmon, 14-Jun-2011.) Reduce axiom usage. (Revised by Wolf Lammen, 24-Jul-2023.)

Conclusion
\( \vdash [ y' / x ] \, z' \in x \leftrightarrow z' \in y' \)
Proof
l0
elequ2
\( \vdash x = w \rightarrow (z' \in x \leftrightarrow z' \in w) \)
elequ2
\( \vdash w = y' \rightarrow (z' \in w \leftrightarrow z' \in y') \)
sbievw2 l0 _