Theorem nfcsb1 3905

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

Syntax hints:  ⊤wtru 1534  Ⅎwnfc 2961  ⦋csb 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sbc 3772  df-csb 3883

This theorem is referenced by:  nfcsb1v  3906  iundisj  24148  disjabrex  30331  disjabrexf  30332  iundisjf  30338  iundisjfi  30518  rdgssun  34658  disjinfi  41452  fsumsplit1  41851  fsumsermpt  41858  climsubmpt  41939  climeldmeqmpt  41947  climfveqmpt  41950  climfveqmpt3  41961  climeldmeqmpt3  41968  climinf2mpt  41993  climinfmpt  41994  dvmptmulf  42220  dvnmptdivc  42221  sge0f1o  42663  sge0lempt  42691  sge0isummpt2  42713  meadjiun  42747  hoimbl2  42946  vonhoire  42953