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

Theorem nfcsb1v 3450
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by NM, 17-Aug-2006.) (Revised by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
nfcsb1v
Distinct variable group:   ,

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2619 . 2
21nfcsb1 3449 1
Colors of variables: wff setvar class
Syntax hints:  F/_wnfc 2605  [_csb 3434
This theorem is referenced by:  csbhypf  3453  csbiebt  3454  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  sbcnestgf  3839  csbnest1g  3845  csbun  3857  csbungOLD  3858  csbin  3860  csbingOLD  3861  csbif  3991  csbifgOLD  3992  csbopg  4235  disjors  4438  disjxiun  4449  disjxun  4450  sbcbr123  4503  sbcbrgOLD  4504  eusvnf  4647  reusv2lem4  4656  reusv2  4658  moop2  4747  pofun  4821  opeliunxp  5056  elrnmpt1  5256  csbima12  5359  csbima12gOLD  5360  fvmpts  5958  fvmpt2i  5962  fvmptex  5966  fmptco  6064  fmptcof  6065  fmptcos  6066  elabrex  6155  fliftfuns  6212  csbov123  6330  csbovgOLD  6332  ovmpt2s  6426  ofmpteq  6558  mpt2mptsx  6863  dmmpt2ssx  6865  fmpt2x  6866  offval22  6879  ovmptss  6881  fmpt2co  6883  dfmpt2  6890  mpt2curryd  7017  mpt2curryvald  7018  fvmpt2curryd  7019  eqerlem  7362  qliftfuns  7417  mptelixpg  7526  boxcutc  7532  xpf1o  7699  iunfi  7828  wdom2d  8027  ixpiunwdom  8038  hsmexlem2  8828  ac6num  8880  ac6c4  8882  iundom2g  8936  seqof2  12165  rlimcld2  13401  nfsum1  13512  sumeq2ii  13515  summolem3  13536  summolem2a  13537  zsum  13540  fsum  13542  sumss2  13548  fsumcvg2  13549  fsumzcl2  13560  sumsn  13563  sumsns  13565  fsummsnunz  13569  fsumsplitsnun  13570  fsum2dlem  13585  fsumcom2  13589  fsumshftm  13596  fsum0diag2  13598  fsum00  13612  fsumabs  13615  fsumrlim  13625  fsumo1  13626  o1fsum  13627  fsumiun  13635  infcvgaux1i  13668  nfcprod1  13717  prodeq2ii  13720  prodmolem3  13740  prodmolem2a  13741  zprod  13744  fprod  13748  fprodntriv  13749  prodss  13754  fprodser  13756  prodsn  13767  fprodm1s  13774  fprodp1s  13775  prodsns  13776  fprodabs  13778  fprodn0  13783  fprod2dlem  13784  fprodcom2  13788  fprodefsum  13830  pcmpt  14411  pcmptdvds  14413  natpropd  15345  fucpropd  15346  gsummpt1n0  16992  gsumcom2  17003  gsummptnn0fz  17014  dprd2d2  17093  psrass1lem  18029  mpfrcl  18187  coe1fzgsumdlem  18343  gsummoncoe1  18346  gsumply1eq  18347  evl1gsumdlem  18392  mdetralt2  19111  mdetunilem2  19115  madugsum  19145  fiuncmp  19904  ptcld  20114  ptcldmpt  20115  ptclsg  20116  elmptrab  20328  prdsdsf  20870  prdsxmet  20872  fsumcn  21374  fsum2cn  21375  ovolfiniun  21912  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  ovoliunnul  21918  finiunmbl  21954  volfiniun  21957  iundisj  21958  iundisj2  21959  iunmbl  21963  iunmbl2  21967  itgss3  22221  itgfsum  22233  itgabs  22241  limciun  22298  dvmptfsum  22376  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlim  22432  dvfsumrlim2  22433  dvfsum2  22435  itgsubstlem  22449  itgsubst  22450  rlimcnp2  23296  fsumdvdscom  23461  fsumdvdsmul  23471  fsumvma  23488  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  disjorsf  27441  disjabrex  27443  disjabrexf  27444  iundisjf  27448  iundisj2f  27449  disjunsn  27453  suppss2f  27477  fmptdF  27495  resmptf  27497  fvmpt2f  27498  fmptcof2  27502  funcnv4mpt  27512  f1od2  27547  iundisjfi  27601  iundisj2fi  27602  gsummpt2co  27771  gsumvsca1  27773  gsumvsca2  27774  esumpfinvalf  28082  measiun  28189  voliune  28201  volfiniune  28202  sbcaltop  29631  finixpnum  30038  ptrest  30048  mbfposadd  30062  itgabsnc  30084  ftc1cnnclem  30088  ftc2nc  30099  mzpsubst  30681  rabdiophlem2  30735  elnn0rabdioph  30736  dvdsrabdioph  30743  fphpd  30750  monotuz  30877  oddcomabszz  30880  wdom2d2  30977  aomclem6  31005  flcidc  31123  fsumcnf  31396  sumsnd  31401  elabrexg  31430  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  sumsnf  31570  fsumnncl  31572  prodsnf  31587  fproddivf  31588  fprodsplitf  31589  fprodcllemf  31591  fprodexp  31600  fprodabs2  31602  fprodle  31604  mccllem  31605  fprodcncf  31704  dvmptmulf  31734  dvnmptdivc  31735  dvmptfprod  31742  iblsplitf  31769  fourierdlem86  31975  fourierdlem112  32001  csbafv12g  32222  csbaovg  32265  fsummsndifre  32345  fsumsplitsndif  32346  fsummmodsndifre  32347  fsummmodsnunz  32348  opeliun2xp  32922  dmmpt2ssx2  32926  bj-sbeqALT  34467  fsumshftd  34682  fsumshftdOLD  34683  riotasv2s  34689  cdleme31sn  36106  cdleme31sn1  36107  cdleme31se2  36109  cdleme32fva  36163  cdleme42b  36204  hlhilset  37664
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