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 -> B = C )
	csbie2g.2	|- ( y = A -> C = D )
Assertion	csbie2g	|- ( A e. V -> [_ A / x ]_ B = D )

Proof

Step	Hyp	Ref	Expression
1		csbie2g.1	|- ( x = y -> B = C )
2		csbie2g.2	|- ( y = A -> C = D )
3		df-csb	|- [_ A / x ]_ B = { z | [. A / x ]. z e. B }
4	1	eleq2d	|- ( x = y -> ( z e. B <-> z e. C ) )
5	2	eleq2d	|- ( y = A -> ( z e. C <-> z e. D ) )
6	4 5	sbcie2g	|- ( A e. V -> ( [. A / x ]. z e. B <-> z e. D ) )
7	6	abbi1dv	|- ( A e. V -> { z | [. A / x ]. z e. B } = D )
8	3 7	eqtrid	|- ( A e. V -> [_ A / x ]_ B = D )