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

Theorem nfcsb1v 3436
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 2616 . 2  |-  F/_ x A
21nfcsb1 3435 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2602   [_csb 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-sbc 3325  df-csb 3421
This theorem is referenced by:  csbhypf  3439  csbiebt  3440  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  sbcnestgf  3834  csbnest1g  3840  csbun  3848  csbin  3849  csbif  3979  csbopg  4221  disjors  4425  invdisjrab  4429  disjxiun  4436  disjxun  4437  sbcbr123  4490  eusvnf  4632  reusv2lem4  4641  reusv2  4643  moop2  4731  pofun  4805  opeliunxp  5040  elrnmpt1  5240  csbima12  5342  csbima12gOLD  5343  fvmpts  5933  fvmpt2i  5938  fvmptex  5942  fmptco  6040  fmptcof  6041  fmptcos  6042  elabrex  6130  fliftfuns  6187  csbov123  6304  ovmpt2s  6399  ofmpteq  6531  mpt2mptsx  6836  dmmpt2ssx  6838  fmpt2x  6839  offval22  6852  ovmptss  6854  fmpt2co  6856  dfmpt2  6863  mpt2curryd  6990  mpt2curryvald  6991  fvmpt2curryd  6992  eqerlem  7335  qliftfuns  7390  mptelixpg  7499  boxcutc  7505  xpf1o  7672  iunfi  7800  wdom2d  7998  ixpiunwdom  8009  hsmexlem2  8798  ac6num  8850  ac6c4  8852  iundom2g  8906  seqof2  12150  rlimcld2  13486  nfsum1  13597  sumeq2ii  13600  summolem3  13621  summolem2a  13622  zsum  13625  fsum  13627  sumss2  13633  fsumcvg2  13634  fsumzcl2  13645  sumsn  13648  sumsns  13650  fsummsnunz  13654  fsumsplitsnun  13655  fsum2dlem  13670  fsumcom2  13674  fsumshftm  13681  fsum0diag2  13683  fsum00  13697  fsumabs  13700  fsumrlim  13710  fsumo1  13711  o1fsum  13712  fsumiun  13720  infcvgaux1i  13753  nfcprod1  13802  prodeq2ii  13805  prodmolem3  13825  prodmolem2a  13826  zprod  13829  fprod  13833  fprodntriv  13834  prodss  13839  fprodser  13841  prodsn  13852  fprodm1s  13859  fprodp1s  13860  prodsns  13861  fprodabs  13863  fprodn0  13868  fprod2dlem  13869  fprodcom2  13873  fprodefsum  13915  pcmpt  14498  pcmptdvds  14500  natpropd  15467  fucpropd  15468  gsummpt1n0  17191  gsumcom2  17202  gsummptnn0fz  17212  dprd2d2  17291  psrass1lem  18227  mpfrcl  18385  coe1fzgsumdlem  18541  gsummoncoe1  18544  gsumply1eq  18545  evl1gsumdlem  18590  mdetralt2  19281  mdetunilem2  19285  madugsum  19315  fiuncmp  20074  ptcld  20283  ptcldmpt  20284  ptclsg  20285  elmptrab  20497  prdsdsf  21039  prdsxmet  21041  fsumcn  21543  fsum2cn  21544  ovolfiniun  22081  ovoliunlem3  22084  ovoliun  22085  ovoliun2  22086  ovoliunnul  22087  finiunmbl  22123  volfiniun  22126  iundisj  22127  iundisj2  22128  iunmbl  22132  iunmbl2  22136  itgss3  22390  itgfsum  22402  itgabs  22410  limciun  22467  dvmptfsum  22545  dvfsumle  22591  dvfsumabs  22593  dvfsumlem1  22596  dvfsumlem2  22597  dvfsumlem3  22598  dvfsumlem4  22599  dvfsumrlim  22601  dvfsumrlim2  22602  dvfsum2  22604  itgsubstlem  22618  itgsubst  22619  rlimcnp2  23497  fsumdvdscom  23662  fsumdvdsmul  23672  fsumvma  23689  dchrisumlema  23874  dchrisumlem2  23876  dchrisumlem3  23877  disjorsf  27654  disjabrex  27656  disjabrexf  27657  iundisjf  27662  iundisj2f  27663  disjunsn  27667  suppss2f  27701  fmptdF  27719  resmptf  27722  fvmpt2f  27723  fmptcof2  27727  acunirnmpt2f  27731  aciunf1lem  27732  funcnv4mpt  27742  f1od2  27781  iundisjfi  27838  iundisj2fi  27839  gsummpt2co  28008  gsumvsca1  28011  gsumvsca2  28012  esumpfinvalf  28308  esum2dlem  28324  esumiun  28326  measiun  28429  voliune  28441  volfiniune  28442  sbcaltop  29862  finixpnum  30281  ptrest  30291  mbfposadd  30305  itgabsnc  30327  ftc1cnnclem  30331  ftc2nc  30342  mzpsubst  30923  rabdiophlem2  30978  elnn0rabdioph  30979  dvdsrabdioph  30986  fphpd  30992  monotuz  31119  oddcomabszz  31122  wdom2d2  31219  aomclem6  31247  flcidc  31367  fsumcnf  31639  sumsnd  31644  elabrexg  31673  fsumclf  31809  fsumsplitf  31810  fsummulc1f  31811  sumsnf  31812  fsumnncl  31814  prodsnf  31829  fproddivf  31830  fprodsplitf  31831  fprodcllemf  31833  fprodexp  31842  fprodabs2  31844  fprodle  31846  mccllem  31847  fprodcncf  31946  dvmptmulf  31976  dvnmptdivc  31977  dvmptfprod  31984  iblsplitf  32011  fourierdlem86  32217  fourierdlem112  32243  csbafv12g  32464  csbaovg  32507  fsummsndifre  32736  fsumsplitsndif  32737  fsummmodsndifre  32738  fsummmodsnunz  32739  opeliun2xp  33195  dmmpt2ssx2  33199  csbingOLD  34038  bj-sbeqALT  34887  fsumshftd  35098  fsumshftdOLD  35099  riotasv2s  35105  cdleme31sn  36522  cdleme31sn1  36523  cdleme31se2  36525  cdleme32fva  36579  cdleme42b  36620  hlhilset  38080  csbcog  38191
  Copyright terms: Public domain W3C validator