Theorem elsb1

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	$$⊢\left[y/x\right]x\in z\leftrightarrow y\in z$$

Proof

Step	Hyp	Ref	Expression
1		elequ1	$$⊢x=w\to \left(x\in z\leftrightarrow w\in z\right)$$
2		elequ1	$$⊢w=y\to \left(w\in z\leftrightarrow y\in z\right)$$
3	1 2	sbievw2	$$⊢\left[y/x\right]x\in z\leftrightarrow y\in z$$