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 e. _V
	csbie2t.2	|- B e. _V
	csbie2.3	|- ( ( x = A /\ y = B ) -> C = D )
Assertion	csbie2	|- [_ A / x ]_ [_ B / y ]_ C = D

Proof

Step	Hyp	Ref	Expression
1		csbie2t.1	|- A e. _V
2		csbie2t.2	|- B e. _V
3		csbie2.3	|- ( ( x = A /\ y = B ) -> C = D )
4	3	gen2	|- A. x A. y ( ( x = A /\ y = B ) -> C = D )
5	1 2	csbie2t	|- ( A. x A. y ( ( x = A /\ y = B ) -> C = D ) -> [_ A / x ]_ [_ B / y ]_ C = D )
6	4 5	ax-mp	|- [_ A / x ]_ [_ B / y ]_ C = D