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 2908  ⦋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 2733

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 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-sbc 3740  df-csb 3848

This theorem is used by:  nfcsb1v  3871  fsumsplit1  15891  iundisj  25849  disjabrex  33158  disjabrexf  33159  iundisjf  33165  iundisjfi  33370  rdgssun  38269  evl1gprodd  43135  disjinfi  46150  fsumsermpt  46535  climsubmpt  46614  climeldmeqmpt  46622  climfveqmpt  46625  climfveqmpt3  46636  climeldmeqmpt3  46643  climinf2mpt  46668  climinfmpt  46669  dvmptmulf  46891  dvnmptdivc  46892  sge0lempt  47364  sge0isummpt2  47386  meadjiun  47420  hoimbl2  47619  vonhoire  47626