Theorem clelsb2

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

Proof

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