MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcsb1 Unicode version

Theorem nfcsb1 3112
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
Hypothesis
Ref Expression
nfcsb1.1  |-  F/_ x A
Assertion
Ref Expression
nfcsb1  |-  F/_ x [_ A  /  x ]_ B

Proof of Theorem nfcsb1
StepHypRef Expression
1 nfcsb1.1 . . . 4  |-  F/_ x A
21a1i 10 . . 3  |-  (  T. 
->  F/_ x A )
32nfcsb1d 3111 . 2  |-  (  T. 
->  F/_ x [_ A  /  x ]_ B )
43trud 1314 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff set class
Syntax hints:    T. wtru 1307   F/_wnfc 2406   [_csb 3081
This theorem is referenced by:  nfcsb1v  3113  pcmpt  12940  iundisj  18905  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem4  19376  dvfsum2  19381  dchrisumlem2  20639  disjabrex  23359  disjabrexf  23360  iundisjfi  23363  iundisjf  23365  measiun  23545  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-sbc 2992  df-csb 3082
  Copyright terms: Public domain W3C validator