Theorem nfcsb 3414

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

Syntax hints:   T. wtru 1371   F/_wnfc 2602   [_csb 3396

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-sbc 3295  df-csb 3397

This theorem is referenced by:  cbvralcsf  3428  cbvreucsf  3430  cbvrabcsf  3431  fmptcof  5987  mpt2mptsx  6748  dmmpt2ssx  6750  fmpt2x  6751  fmpt2co  6767  dfmpt2  6774  mpt2curryd  6899  fvmpt2curryd  6901  nfsum  13287  fsum2dlem  13356  fsumcom2  13360  fsumcn  20579  fsum2cn  20580  dvmptfsum  21581  itgsubst  21655  iundisj2f  26084  f1od2  26176  nfcprod  27569  fprod2dlem  27636  fprodcom2  27640  wdom2d2  29533  elfvmptrab1  30303  elovmpt2rab1  30308  dmmpt2ssx2  30876  cdlemkid  34919  cdlemk19x  34926  cdlemk11t  34929