Theorem sbc2iegf

Description: Conversion of implicit substitution to explicit class substitution. (Contributed by Mario Carneiro, 19-Dec-2013)

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

Proof

Step	Hyp	Ref	Expression
1		sbc2iegf.1	$$⊢Ⅎx\psi$$
2		sbc2iegf.2	$$⊢Ⅎy\psi$$
3		sbc2iegf.3	$$⊢ℲxB\in W$$
4		sbc2iegf.4	$$⊢\left(x=A\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
5		simpl	$$⊢\left(A\in V\wedge B\in W\right)\to A\in V$$
6		simpl	$$⊢\left(B\in W\wedge x=A\right)\to B\in W$$
7	4	adantll	$$⊢\left(\left(B\in W\wedge x=A\right)\wedge y=B\right)\to \left(\phi \leftrightarrow \psi \right)$$
8		nfv	$$⊢Ⅎy\left(B\in W\wedge x=A\right)$$
9	2	a1i	$$⊢\left(B\in W\wedge x=A\right)\to Ⅎy\psi$$
10	6 7 8 9	sbciedf	$$⊢\left(B\in W\wedge x=A\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
11	10	adantll	$$⊢\left(\left(A\in V\wedge B\in W\right)\wedge x=A\right)\to \left(\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$
12		nfv	$$⊢ℲxA\in V$$
13	12 3	nfan	$$⊢Ⅎx\left(A\in V\wedge B\in W\right)$$
14	1	a1i	$$⊢\left(A\in V\wedge B\in W\right)\to Ⅎx\psi$$
15	5 11 13 14	sbciedf	$$⊢\left(A\in V\wedge B\in W\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\underset{\dot{}}{[}B/y\underset{\dot{}}{]}\phi \leftrightarrow \psi \right)$$