Theorem sbcie2g

Description: Conversion of implicit substitution to explicit class substitution. This version of sbcie avoids a disjointness condition on x , A by substituting twice. (Contributed by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	sbcie2g.1	|- ( x = y -> ( ph <-> ps ) )
	sbcie2g.2	|- ( y = A -> ( ps <-> ch ) )
Assertion	sbcie2g	|- ( A e. V -> ( [. A / x ]. ph <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		sbcie2g.1	|- ( x = y -> ( ph <-> ps ) )
2		sbcie2g.2	|- ( y = A -> ( ps <-> ch ) )
3		dfsbcq	|- ( y = A -> ( [. y / x ]. ph <-> [. A / x ]. ph ) )
4		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
5	1	sbievw	|- ( [ y / x ] ph <-> ps )
6	4 5	bitr3i	|- ( [. y / x ]. ph <-> ps )
7	3 2 6	vtoclbg	|- ( A e. V -> ( [. A / x ]. ph <-> ch ) )