Theorem nfcsb1 3869

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

This proof depends on syntax axioms:  ⊤wtru 1570  Ⅎwnfc 2907  ⦋csb 3846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-sbc 3739  df-csb 3847

This theorem is used by:  nfcsb1v  3870  fsumsplit1  15916  iundisj  25874  disjabrex  33223  disjabrexf  33224  iundisjf  33230  iundisjfi  33434  rdgssun  38394  evl1gprodd  43260  disjinfi  46300  fsumsermpt  46684  climsubmpt  46763  climeldmeqmpt  46771  climfveqmpt  46774  climfveqmpt3  46785  climeldmeqmpt3  46792  climinf2mpt  46817  climinfmpt  46818  dvmptmulf  47040  dvnmptdivc  47041  sge0lempt  47513  sge0isummpt2  47535  meadjiun  47569  hoimbl2  47768  vonhoire  47775