Theorem csbie2t

Description: Conversion of implicit substitution to explicit substitution into a class (closed form of csbie2 ). (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 13-Oct-2016)

	Ref	Expression
Hypotheses	csbie2t.1	$$⊢A\in \mathrm{V}$$
	csbie2t.2	$$⊢B\in \mathrm{V}$$
Assertion	csbie2t	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\to ⦋A/x⦌⦋B/y⦌C=D$$

Proof

Step	Hyp	Ref	Expression
1		csbie2t.1	$$⊢A\in \mathrm{V}$$
2		csbie2t.2	$$⊢B\in \mathrm{V}$$
3		nfa1	$$⊢Ⅎx\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)$$
4		nfcvd	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\to \underset{\_}{Ⅎ}xD$$
5	1	a1i	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\to A\in \mathrm{V}$$
6		nfa2	$$⊢Ⅎy\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)$$
7		nfv	$$⊢Ⅎyx=A$$
8	6 7	nfan	$$⊢Ⅎy\left(\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\wedge x=A\right)$$
9		nfcvd	$$⊢\left(\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\wedge x=A\right)\to \underset{\_}{Ⅎ}yD$$
10	2	a1i	$$⊢\left(\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\wedge x=A\right)\to B\in \mathrm{V}$$
11		2sp	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\to \left(\left(x=A\wedge y=B\right)\to C=D\right)$$
12	11	impl	$$⊢\left(\left(\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\wedge x=A\right)\wedge y=B\right)\to C=D$$
13	8 9 10 12	csbiedf	$$⊢\left(\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\wedge x=A\right)\to ⦋B/y⦌C=D$$
14	3 4 5 13	csbiedf	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\to ⦋A/x⦌⦋B/y⦌C=D$$