Theorem nfcsb1 3889

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

Syntax hints:  ⊤wtru 1538  Ⅎwnfc 2957  ⦋csb 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-sbc 3759  df-csb 3867

This theorem is referenced by:  nfcsb1v  3890  iundisj  24127  disjabrex  30313  disjabrexf  30314  iundisjf  30320  iundisjfi  30500  rdgssun  34670  disjinfi  41539  fsumsplit1  41938  fsumsermpt  41945  climsubmpt  42026  climeldmeqmpt  42034  climfveqmpt  42037  climfveqmpt3  42048  climeldmeqmpt3  42055  climinf2mpt  42080  climinfmpt  42081  dvmptmulf  42307  dvnmptdivc  42308  sge0f1o  42749  sge0lempt  42777  sge0isummpt2  42799  meadjiun  42833  hoimbl2  43032  vonhoire  43039