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

Theorem nfcsb1v 3303
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  |-  F/_ x [_ A  /  x ]_ B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2578 . 2  |-  F/_ x A
21nfcsb1 3302 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2565   [_csb 3287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-sbc 3186  df-csb 3288
This theorem is referenced by:  csbhypf  3306  csbiebt  3307  cbvralcsf  3318  cbvreucsf  3320  cbvrabcsf  3321  sbcnestgf  3690  csbnest1g  3696  csbun  3708  csbungOLD  3709  csbin  3711  csbingOLD  3712  csbif  3838  csbifgOLD  3839  csbopg  4076  disjors  4277  disjxiun  4288  disjxun  4289  sbcbr123  4342  sbcbrgOLD  4343  eusvnf  4486  reusv2lem4  4495  reusv2  4497  moop2  4585  pofun  4656  opeliunxp  4889  elrnmpt1  5087  csbima12  5185  csbima12gOLD  5186  fvmpts  5775  fvmpt2i  5779  fvmptex  5783  fmptco  5875  fmptcof  5876  fmptcos  5877  elabrex  5959  fliftfuns  6006  csbov123  6121  csbovgOLD  6123  ovmpt2s  6213  ofmpteq  6337  mpt2mptsx  6636  dmmpt2ssx  6638  fmpt2x  6639  offval22  6651  ovmptss  6653  fmpt2co  6655  dfmpt2  6662  mpt2curryd  6787  mpt2curryvald  6788  fvmpt2curryd  6789  eqerlem  7132  qliftfuns  7186  mptelixpg  7299  boxcutc  7305  xpf1o  7472  iunfi  7598  wdom2d  7794  ixpiunwdom  7805  hsmexlem2  8595  ac6num  8647  ac6c4  8649  iundom2g  8703  seqof2  11863  rlimcld2  13055  nfsum1  13166  sumeq2w  13168  sumeq2ii  13169  summolem3  13190  summolem2a  13191  zsum  13194  fsum  13196  sumss2  13202  fsumcvg2  13203  sumsn  13216  sumsns  13218  fsum2dlem  13236  fsumcom2  13240  fsumshftm  13247  fsum0diag2  13249  fsum00  13260  fsumabs  13263  fsumrlim  13273  fsumo1  13274  o1fsum  13275  fsumiun  13283  infcvgaux1i  13318  pcmpt  13953  pcmptdvds  13955  natpropd  14885  fucpropd  14886  gsummpt1n0  16455  gsumcom2  16466  dprd2d2  16542  psrass1lem  17446  mpfrcl  17603  evl1gsumdlem  17789  mdetralt2  18414  mdetunilem2  18418  madugsum  18448  fiuncmp  19006  ptcld  19185  ptcldmpt  19186  ptclsg  19187  elmptrab  19399  prdsdsf  19941  prdsxmet  19943  fsumcn  20445  fsum2cn  20446  ovolfiniun  20983  ovoliunlem3  20986  ovoliun  20987  ovoliun2  20988  ovoliunnul  20989  finiunmbl  21024  volfiniun  21027  iundisj  21028  iundisj2  21029  iunmbl  21033  iunmbl2  21037  itgss3  21291  itgfsum  21303  itgabs  21311  limciun  21368  dvmptfsum  21446  dvfsumle  21492  dvfsumabs  21494  dvfsumlem1  21497  dvfsumlem2  21498  dvfsumlem3  21499  dvfsumlem4  21500  dvfsumrlim  21502  dvfsumrlim2  21503  dvfsum2  21505  itgsubstlem  21519  itgsubst  21520  rlimcnp2  22359  fsumdvdscom  22524  fsumdvdsmul  22534  fsumvma  22551  dchrisumlema  22736  dchrisumlem2  22738  dchrisumlem3  22739  disjorsf  25923  disjabrex  25925  disjabrexf  25926  iundisjf  25930  iundisj2f  25931  suppss2f  25953  fmptdF  25971  resmptf  25973  fvmpt2f  25974  fmptcof2  25978  funcnv4mpt  25988  iundisjfi  26079  iundisj2fi  26080  gsummpt2co  26248  gsumvsca1  26250  gsumvsca2  26251  esumpfinvalf  26524  measiun  26631  voliune  26644  volfiniune  26645  nfcprod1  27422  prodeq2w  27424  prodeq2ii  27425  prodmolem3  27445  prodmolem2a  27446  zprod  27449  fprod  27453  fprodntriv  27454  prodss  27459  fprodser  27461  prodsn  27472  fprodm1s  27479  fprodp1s  27480  prodsns  27481  fprodabs  27483  fprodefsum  27484  fprodn0  27489  fprod2dlem  27490  fprodcom2  27494  sbcaltop  28011  finixpnum  28412  ptrest  28423  mbfposadd  28437  itgabsnc  28459  ftc1cnnclem  28463  ftc2nc  28474  mzpsubst  29083  rabdiophlem2  29138  elnn0rabdioph  29139  dvdsrabdioph  29146  fphpd  29153  monotuz  29280  oddcomabszz  29283  wdom2d2  29382  aomclem6  29410  flcidc  29529  fsumcnf  29741  sumsnd  29746  csbafv12g  30041  csbaovg  30084  fsumz  30234  fsummsndifre  30235  fsumsplitsndif  30236  fsummmodsndifre  30237  fsummsnunz  30239  fsumsplitsnun  30240  fsummmodsnunre  30241  opeliun2xp  30718  dmmpt2ssx2  30725  gsummptnn0fz  30804  coe1fzgsumdlem  30835  gsummoncoe1  30841  bj-sbeqALT  32400  fsumshftd  32600  fsumshftdOLD  32601  riotasv2s  32607  cdleme31sn  34022  cdleme31sn1  34023  cdleme31se2  34025  cdleme32fva  34079  cdleme42b  34120  hlhilset  35580
  Copyright terms: Public domain W3C validator