Theorem csbie2g

Description: Conversion of implicit substitution to explicit class substitution. This version of csbie avoids a disjointness condition on x , A and x , D by substituting twice. (Contributed by Mario Carneiro, 11-Nov-2016)

	Ref	Expression
Hypotheses	csbie2g.1	$$⊢x=y\to B=C$$
	csbie2g.2	$$⊢y=A\to C=D$$
Assertion	csbie2g	$$⊢A\in V\to ⦋A/x⦌B=D$$

Proof

Step	Hyp	Ref	Expression
1		csbie2g.1	$$⊢x=y\to B=C$$
2		csbie2g.2	$$⊢y=A\to C=D$$
3		df-csb	$$⊢⦋A/x⦌B=\left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B\right\}$$
4	1	eleq2d	$$⊢x=y\to \left(z\in B\leftrightarrow z\in C\right)$$
5	2	eleq2d	$$⊢y=A\to \left(z\in C\leftrightarrow z\in D\right)$$
6	4 5	sbcie2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B\leftrightarrow z\in D\right)$$
7	6	abbi1dv	$$⊢A\in V\to \left\{z|\underset{\dot{}}{[}A/x\underset{\dot{}}{]}z\in B\right\}=D$$
8	3 7	eqtrid	$$⊢A\in V\to ⦋A/x⦌B=D$$