Theorem nfcsb 3551

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 1730	. . 3 ⊢ Ⅎ𝑦⊤
2		nfcsb.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfcsb.2	. . . 4 ⊢ Ⅎ𝑥𝐵
5	4	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
6	1, 3, 5	nfcsbd 3550	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵)
7	6	trud 1493	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑦⦌𝐵

Syntax hints:  ⊤wtru 1484  Ⅎwnfc 2751  ⦋csb 3533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-sbc 3436  df-csb 3534

This theorem is referenced by:  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  elfvmptrab1  6305  fmptcof  6397  elovmpt2rab1  6881  mpt2mptsx  7233  dmmpt2ssx  7235  fmpt2x  7236  el2mpt2csbcl  7250  fmpt2co  7260  dfmpt2  7267  mpt2curryd  7395  fvmpt2curryd  7397  nfsum  14421  fsum2dlem  14501  fsumcom2  14505  fsumcom2OLD  14506  nfcprod  14641  fprod2dlem  14710  fprodcom2  14714  fprodcom2OLD  14715  fsumcn  22673  fsum2cn  22674  dvmptfsum  23738  itgsubst  23812  iundisj2f  29403  f1od2  29499  esumiun  30156  poimirlem26  33435  cdlemkid  36224  cdlemk19x  36231  cdlemk11t  36234  wdom2d2  37602  dmmpt2ssx2  42115