Theorem nfcsb1 3856

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

Syntax hints:  ⊤wtru 1540  Ⅎwnfc 2887  ⦋csb 3832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-sbc 3717  df-csb 3833

This theorem is referenced by:  nfcsb1v  3857  fsumsplit1  15457  iundisj  24712  disjabrex  30921  disjabrexf  30922  iundisjf  30928  iundisjfi  31117  rdgssun  35549  disjinfi  42731  fsumsermpt  43120  climsubmpt  43201  climeldmeqmpt  43209  climfveqmpt  43212  climfveqmpt3  43223  climeldmeqmpt3  43230  climinf2mpt  43255  climinfmpt  43256  dvmptmulf  43478  dvnmptdivc  43479  sge0f1o  43920  sge0lempt  43948  sge0isummpt2  43970  meadjiun  44004  hoimbl2  44203  vonhoire  44210