Theorem nfcsb1 3877

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 3876	. 2 ⊢ (⊤ → Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵)
4	3	mptru 1577	1 ⊢ Ⅎ𝑥⦋𝐴 / 𝑥⦌𝐵

Syntax hints:  ⊤wtru 1571  Ⅎwnfc 2910  ⦋csb 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-sbc 3746  df-csb 3855

This theorem is referenced by:  nfcsb1v  3878  fsumsplit1  15798  iundisj  25688  disjabrex  32908  disjabrexf  32909  iundisjf  32915  iundisjfi  33122  rdgssun  38005  evl1gprodd  42865  disjinfi  45893  fsumsermpt  46278  climsubmpt  46357  climeldmeqmpt  46365  climfveqmpt  46368  climfveqmpt3  46379  climeldmeqmpt3  46386  climinf2mpt  46411  climinfmpt  46412  dvmptmulf  46634  dvnmptdivc  46635  sge0lempt  47107  sge0isummpt2  47129  meadjiun  47163  hoimbl2  47362  vonhoire  47369