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

Theorem nfcsb1 3125
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 3124 . 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 2419   [_csb 3094
This theorem is referenced by:  nfcsb1v  3126  pcmpt  12956  iundisj  18921  dvfsumabs  19386  dvfsumlem2  19390  dvfsumlem4  19392  dvfsum2  19397  dchrisumlem2  20655  disjabrex  23374  disjabrexf  23375  iundisjfi  23378  iundisjf  23380  measiun  23560  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-sbc 3005  df-csb 3095
  Copyright terms: Public domain W3C validator