Theorem nfcsb1 3870

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnfc 2907  ⦋csb 3847

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-sbc 3740  df-csb 3848

This theorem is used by:  nfcsb1v  3871  fsumsplit1  15831  iundisj  25776  disjabrex  33055  disjabrexf  33056  iundisjf  33062  iundisjfi  33267  rdgssun  38132  evl1gprodd  42983  disjinfi  46024  fsumsermpt  46409  climsubmpt  46488  climeldmeqmpt  46496  climfveqmpt  46499  climfveqmpt3  46510  climeldmeqmpt3  46517  climinf2mpt  46542  climinfmpt  46543  dvmptmulf  46765  dvnmptdivc  46766  sge0lempt  47238  sge0isummpt2  47260  meadjiun  47294  hoimbl2  47493  vonhoire  47500