Theorem nfcsb1 3945

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

Syntax hints:  ⊤wtru 1538  Ⅎwnfc 2893  ⦋csb 3921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-sbc 3805  df-csb 3922

This theorem is referenced by:  nfcsb1v  3946  fsumsplit1  15793  iundisj  25602  disjabrex  32604  disjabrexf  32605  iundisjf  32611  iundisjfi  32801  rdgssun  37344  evl1gprodd  42074  disjinfi  45099  fsumsermpt  45500  climsubmpt  45581  climeldmeqmpt  45589  climfveqmpt  45592  climfveqmpt3  45603  climeldmeqmpt3  45610  climinf2mpt  45635  climinfmpt  45636  dvmptmulf  45858  dvnmptdivc  45859  sge0f1o  46303  sge0lempt  46331  sge0isummpt2  46353  meadjiun  46387  hoimbl2  46586  vonhoire  46593