Theorem nfcsb 3517

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

Hypotheses

Ref	Expression
nfcsb.1	⊢ Ⅎ𝑥𝐴
nfcsb.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfcsb	⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Proof of Theorem nfcsb

Step	Hyp	Ref	Expression
1		nftru 1721	. . 3 ⊢ Ⅎ𝑦⊤
2		nfcsb.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfcsb.2	. . . 4 ⊢ Ⅎ𝑥𝐵
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
6	1, 3, 5	nfcsbd 3516	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
7	6	trud 1484	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1476  Ⅎwnfc 2738  ⦋csb 3499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-sbc 3403  df-csb 3500

This theorem is referenced by:  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  elfvmptrab1  6213  fmptcof  6304  elovmpt2rab1  6779  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  el2mpt2csbcl  7137  fmpt2co  7147  dfmpt2  7154  mpt2curryd  7282  fvmpt2curryd  7284  nfsum  14269  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  nfcprod  14480  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fsumcn  22481  fsum2cn  22482  dvmptfsum  23542  itgsubst  23616  iundisj2f  28785  f1od2  28887  esumiun  29483  poimirlem26  32605  cdlemkid  35242  cdlemk19x  35249  cdlemk11t  35252  wdom2d2  36620  dmmpt2ssx2  41908