Theorem sbcel2

Description: Move proper substitution in and out of a membership relation. (Contributed by NM, 14-Nov-2005) (Revised by NM, 18-Aug-2018)

	Ref	Expression
Assertion	sbcel2	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow B\in ⦋A/x⦌C$$

Proof

Step	Hyp	Ref	Expression
1		sbcel12	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow ⦋A/x⦌B\in ⦋A/x⦌C$$
2		csbconstg	$$⊢A\in \mathrm{V}\to ⦋A/x⦌B=B$$
3	2	eleq1d	$$⊢A\in \mathrm{V}\to \left(⦋A/x⦌B\in ⦋A/x⦌C\leftrightarrow B\in ⦋A/x⦌C\right)$$
4	1 3	bitrid	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow B\in ⦋A/x⦌C\right)$$
5		sbcex	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\to A\in \mathrm{V}$$
6	5	con3i	$$⊢\neg A\in \mathrm{V}\to \neg \underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C$$
7		noel	$$⊢\neg B\in \varnothing$$
8		csbprc	$$⊢\neg A\in \mathrm{V}\to ⦋A/x⦌C=\varnothing$$
9	8	eleq2d	$$⊢\neg A\in \mathrm{V}\to \left(B\in ⦋A/x⦌C\leftrightarrow B\in \varnothing \right)$$
10	7 9	mtbiri	$$⊢\neg A\in \mathrm{V}\to \neg B\in ⦋A/x⦌C$$
11	6 10	2falsed	$$⊢\neg A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow B\in ⦋A/x⦌C\right)$$
12	4 11	pm2.61i	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}B\in C\leftrightarrow B\in ⦋A/x⦌C$$