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
Assertion
Ref Expression
nfcsb1

Proof of Theorem nfcsb1
StepHypRef Expression
1 nfcsb1.1 . . . 4
21a1i 10 . . 3
32nfcsb1d 3124 . 2
43trud 1314 1
 Colors of variables: wff set class Syntax hints:   wtru 1307  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