Theorem nfcsb1 3851

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

Syntax hints:  ⊤wtru 1539  Ⅎwnfc 2936  ⦋csb 3828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-sbc 3721  df-csb 3829

This theorem is referenced by:  nfcsb1v  3852  iundisj  24152  disjabrex  30345  disjabrexf  30346  iundisjf  30352  iundisjfi  30545  rdgssun  34795  disjinfi  41820  fsumsplit1  42214  fsumsermpt  42221  climsubmpt  42302  climeldmeqmpt  42310  climfveqmpt  42313  climfveqmpt3  42324  climeldmeqmpt3  42331  climinf2mpt  42356  climinfmpt  42357  dvmptmulf  42579  dvnmptdivc  42580  sge0f1o  43021  sge0lempt  43049  sge0isummpt2  43071  meadjiun  43105  hoimbl2  43304  vonhoire  43311