Theorem nfcsb1 3878

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

Syntax hints:  ⊤wtru 1564  Ⅎwnfc 2912  ⦋csb 3855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-nf 1807  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-sbc 3748  df-csb 3856

This theorem is referenced by:  nfcsb1v  3879  fsumsplit1  15786  iundisj  25668  disjabrex  32837  disjabrexf  32838  iundisjf  32844  iundisjfi  33053  rdgssun  37884  evl1gprodd  42746  disjinfi  45768  fsumsermpt  46153  climsubmpt  46232  climeldmeqmpt  46240  climfveqmpt  46243  climfveqmpt3  46254  climeldmeqmpt3  46261  climinf2mpt  46286  climinfmpt  46287  dvmptmulf  46509  dvnmptdivc  46510  sge0lempt  46982  sge0isummpt2  47004  meadjiun  47038  hoimbl2  47237  vonhoire  47244