Theorem nfcsb1 3922

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

Syntax hints:  ⊤wtru 1541  Ⅎwnfc 2890  ⦋csb 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-sbc 3789  df-csb 3900

This theorem is referenced by:  nfcsb1v  3923  fsumsplit1  15781  iundisj  25583  disjabrex  32595  disjabrexf  32596  iundisjf  32602  iundisjfi  32798  rdgssun  37379  evl1gprodd  42118  disjinfi  45197  fsumsermpt  45594  climsubmpt  45675  climeldmeqmpt  45683  climfveqmpt  45686  climfveqmpt3  45697  climeldmeqmpt3  45704  climinf2mpt  45729  climinfmpt  45730  dvmptmulf  45952  dvnmptdivc  45953  sge0lempt  46425  sge0isummpt2  46447  meadjiun  46481  hoimbl2  46680  vonhoire  46687