Theorem elsb1

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.)

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