Theorem nfcsb1 3875

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

Hypothesis

Ref	Expression
nfcsb1.1	⊢ Ⅎ𝑥𝐴

Assertion

Ref	Expression
nfcsb1	⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Proof of Theorem nfcsb1

Step	Hyp	Ref	Expression
1		nfcsb1.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3	2	nfcsb1d 3874	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵)
4	3	mptru 1566	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  ⊤wtru 1560  Ⅎwnfc 2908  ⦋csb 3852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3745  df-csb 3853

This theorem is referenced by:  nfcsb1v  3876  fsumsplit1  15755  iundisj  25590  disjabrex  32731  disjabrexf  32732  iundisjf  32738  iundisjfi  32948  rdgssun  37836  evl1gprodd  42698  disjinfi  45734  fsumsermpt  46119  climsubmpt  46198  climeldmeqmpt  46206  climfveqmpt  46209  climfveqmpt3  46220  climeldmeqmpt3  46227  climinf2mpt  46252  climinfmpt  46253  dvmptmulf  46475  dvnmptdivc  46476  sge0lempt  46948  sge0isummpt2  46970  meadjiun  47004  hoimbl2  47203  vonhoire  47210