Theorem nfcsbd

Description: Deduction version of nfcsb . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 21-Nov-2005) (Revised by Mario Carneiro, 12-Oct-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfcsbd.1	|- F/ y ph
	nfcsbd.2	|- ( ph -> F/_ x A )
	nfcsbd.3	|- ( ph -> F/_ x B )
Assertion	nfcsbd	|- ( ph -> F/_ x [_ A / y ]_ B )

Proof

Step	Hyp	Ref	Expression
1		nfcsbd.1	|- F/ y ph
2		nfcsbd.2	|- ( ph -> F/_ x A )
3		nfcsbd.3	|- ( ph -> F/_ x B )
4		df-csb	|- [_ A / y ]_ B = { z | [. A / y ]. z e. B }
5		nfv	|- F/ z ph
6	3	nfcrd	|- ( ph -> F/ x z e. B )
7	1 2 6	nfsbcd	|- ( ph -> F/ x [. A / y ]. z e. B )
8	5 7	nfabd	|- ( ph -> F/_ x { z | [. A / y ]. z e. B } )
9	4 8	nfcxfrd	|- ( ph -> F/_ x [_ A / y ]_ B )