Theorem csbie2

Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by NM, 27-Aug-2007)

	Ref	Expression
Hypotheses	csbie2t.1	$$⊢A\in \mathrm{V}$$
	csbie2t.2	$$⊢B\in \mathrm{V}$$
	csbie2.3	$$⊢\left(x=A\wedge y=B\right)\to C=D$$
Assertion	csbie2	$$⊢⦋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		csbie2.3	$$⊢\left(x=A\wedge y=B\right)\to C=D$$
4	3	gen2	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)$$
5	1 2	csbie2t	$$⊢\forall x\forall y\left(\left(x=A\wedge y=B\right)\to C=D\right)\to ⦋A/x⦌⦋B/y⦌C=D$$
6	4 5	ax-mp	$$⊢⦋A/x⦌⦋B/y⦌C=D$$