Theorem nfcsb1 3879

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

This proof depends on syntax axioms:  ⊤wtru 1571  Ⅎwnfc 2913  ⦋csb 3856

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-sbc 3748  df-csb 3857

This theorem is used by:  nfcsb1v  3880  fsumsplit1  15822  iundisj  25744  disjabrex  32964  disjabrexf  32965  iundisjf  32971  iundisjfi  33178  rdgssun  38065  evl1gprodd  42925  disjinfi  45951  fsumsermpt  46336  climsubmpt  46415  climeldmeqmpt  46423  climfveqmpt  46426  climfveqmpt3  46437  climeldmeqmpt3  46444  climinf2mpt  46469  climinfmpt  46470  dvmptmulf  46692  dvnmptdivc  46693  sge0lempt  47165  sge0isummpt2  47187  meadjiun  47221  hoimbl2  47420  vonhoire  47427