Theorem nfcsb1 3772

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

Syntax hints:  ⊤wtru 1657  Ⅎwnfc 2956  ⦋csb 3757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-sbc 3663  df-csb 3758

This theorem is referenced by:  nfcsb1v  3773  fprodsplit1f  15100  iundisj  23721  disjabrex  29938  disjabrexf  29939  iundisjf  29945  iundisjfi  30098  disjinfi  40183  fsumsplit1  40593  fsumsermpt  40600  climsubmpt  40681  climeldmeqmpt  40689  climfveqmpt  40692  climfveqmpt3  40703  climeldmeqmpt3  40710  climinf2mpt  40735  climinfmpt  40736  dvmptmulf  40941  dvnmptdivc  40942  sge0f1o  41384  sge0lempt  41412  sge0isummpt2  41434  meadjiun  41468  hoimbl2  41667  vonhoire  41674