Theorem sbc2iedv

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 16-Dec-2008) (Proof shortened by Mario Carneiro, 18-Oct-2016)

	Ref	Expression
Hypotheses	sbc2iedv.1	$$⊢A\in \mathrm{V}$$
	sbc2iedv.2	$$⊢B\in \mathrm{V}$$
	sbc2iedv.3	$$⊢\phi \to \left(\left(x=A\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)\right)$$
Assertion	sbc2iedv	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbc2iedv.1	$$⊢A\in \mathrm{V}$$
2		sbc2iedv.2	$$⊢B\in \mathrm{V}$$
3		sbc2iedv.3	$$⊢\phi \to \left(\left(x=A\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)\right)$$
4	1	a1i	$$⊢\phi \to A\in \mathrm{V}$$
5	2	a1i	$$⊢\left(\phi \wedge x=A\right)\to B\in \mathrm{V}$$
6	3	impl	$$⊢\left(\left(\phi \wedge x=A\right)\wedge y=B\right)\to \left(\psi \leftrightarrow \chi \right)$$
7	5 6	sbcied	$$⊢\left(\phi \wedge x=A\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$
8	4 7	sbcied	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\psi \leftrightarrow \chi \right)$$