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\to \left(\phi \leftrightarrow \psi \right)$$
	sbcie2g.2	$$⊢y=A\to \left(\psi \leftrightarrow \chi \right)$$
Assertion	sbcie2g	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcie2g.1	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
2		sbcie2g.2	$$⊢y=A\to \left(\psi \leftrightarrow \chi \right)$$
3		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4		sbsbc	$$⊢\left[y/x\right]\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
5	1	sbievw	$$⊢\left[y/x\right]\phi \leftrightarrow \psi$$
6	4 5	bitr3i	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
7	3 2 6	vtoclbg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \chi \right)$$