Theorem nfcsb 3419

Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)

Hypotheses

Ref	Expression
nfcsb.1	|- F/_ x A
nfcsb.2	|- F/_ x B

Assertion

Ref	Expression
nfcsb	|- F/_ x [_ A / y ]_ B

Proof of Theorem nfcsb

Step	Hyp	Ref	Expression
1		nftru 1673	. . 3 |- F/ y T.
2		nfcsb.1	. . . 4 |- F/_ x A
3	2	a1i 11	. . 3 |- ( T. -> F/_ x A )
4		nfcsb.2	. . . 4 |- F/_ x B
5	4	a1i 11	. . 3 |- ( T. -> F/_ x B )
6	1, 3, 5	nfcsbd 3418	. 2 |- ( T. -> F/_ x [_ A / y ]_ B )
7	6	trud 1446	1 |- F/_ x [_ A / y ]_ B

Syntax hints:   T. wtru 1438   F/_wnfc 2577   [_csb 3401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-sbc 3306  df-csb 3402

This theorem is referenced by:  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  elfvmptrab1  5986  fmptcof  6072  elovmpt2rab1  6530  mpt2mptsx  6870  dmmpt2ssx  6872  fmpt2x  6873  fmpt2co  6890  dfmpt2  6897  mpt2curryd  7024  fvmpt2curryd  7026  nfsum  13735  fsum2dlem  13809  fsumcom2  13813  nfcprod  13943  fprod2dlem  14012  fprodcom2  14016  fsumcn  21798  fsum2cn  21799  dvmptfsum  22804  itgsubst  22878  iundisj2f  28039  f1od2  28152  esumiun  28754  poimirlem26  31670  cdlemkid  34212  cdlemk19x  34219  cdlemk11t  34222  wdom2d2  35596  dmmpt2ssx2  38878