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

Theorem nfcsb 3452
 Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.)
Hypotheses
Ref Expression
nfcsb.1
nfcsb.2
Assertion
Ref Expression
nfcsb

Proof of Theorem nfcsb
StepHypRef Expression
1 nftru 1626 . . 3
2 nfcsb.1 . . . 4
32a1i 11 . . 3
4 nfcsb.2 . . . 4
54a1i 11 . . 3
61, 3, 5nfcsbd 3451 . 2
76trud 1404 1
 Colors of variables: wff setvar class Syntax hints:   wtru 1396  F/_wnfc 2605  [_csb 3434 This theorem is referenced by:  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  elfvmptrab1  5976  fmptcof  6065  elovmpt2rab1  6522  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  fmpt2co  6883  dfmpt2  6890  mpt2curryd  7017  fvmpt2curryd  7019  nfsum  13513  fsum2dlem  13585  fsumcom2  13589  nfcprod  13718  fprod2dlem  13784  fprodcom2  13788  fsumcn  21374  fsum2cn  21375  dvmptfsum  22376  itgsubst  22450  iundisj2f  27449  f1od2  27547  wdom2d2  30977  dmmpt2ssx2  32926  cdlemkid  36662  cdlemk19x  36669  cdlemk11t  36672 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-sbc 3328  df-csb 3435
 Copyright terms: Public domain W3C validator