Theorem nfcsb 3458

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 1609	. . 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 3457	. 2 |- ( T. -> F/_ x [_ A / y ]_ B )
7	6	trud 1388	1 |- F/_ x [_ A / y ]_ B

Syntax hints:   T. wtru 1380   F/_wnfc 2615   [_csb 3440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-sbc 3337  df-csb 3441

This theorem is referenced by:  cbvralcsf  3472  cbvreucsf  3474  cbvrabcsf  3475  elfvmptrab1  5977  fmptcof  6066  elovmpt2rab1  6517  mpt2mptsx  6858  dmmpt2ssx  6860  fmpt2x  6861  fmpt2co  6878  dfmpt2  6885  mpt2curryd  7010  fvmpt2curryd  7012  nfsum  13493  fsum2dlem  13565  fsumcom2  13569  fsumcn  21242  fsum2cn  21243  dvmptfsum  22244  itgsubst  22318  iundisj2f  27263  f1od2  27361  nfcprod  28961  fprod2dlem  29028  fprodcom2  29032  wdom2d2  30896  dmmpt2ssx2  32360  cdlemkid  36088  cdlemk19x  36095  cdlemk11t  36098