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 2605 . 2  |-  F/_ x A
21nfcsb1 3435 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2591   [_csb 3420
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-sbc 3314  df-csb 3421
This theorem is referenced by:  csbhypf  3439  csbiebt  3440  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  sbcnestgf  3825  csbnest1g  3831  csbun  3843  csbungOLD  3844  csbin  3846  csbingOLD  3847  csbif  3976  csbifgOLD  3977  csbopg  4220  disjors  4423  disjxiun  4434  disjxun  4435  sbcbr123  4488  sbcbrgOLD  4489  eusvnf  4632  reusv2lem4  4641  reusv2  4643  moop2  4732  pofun  4806  opeliunxp  5041  elrnmpt1  5241  csbima12  5344  csbima12gOLD  5345  fvmpts  5943  fvmpt2i  5947  fvmptex  5951  fmptco  6049  fmptcof  6050  fmptcos  6051  elabrex  6140  fliftfuns  6197  csbov123  6315  csbovgOLD  6317  ovmpt2s  6411  ofmpteq  6543  mpt2mptsx  6848  dmmpt2ssx  6850  fmpt2x  6851  offval22  6864  ovmptss  6866  fmpt2co  6868  dfmpt2  6875  mpt2curryd  7000  mpt2curryvald  7001  fvmpt2curryd  7002  eqerlem  7345  qliftfuns  7400  mptelixpg  7508  boxcutc  7514  xpf1o  7681  iunfi  7810  wdom2d  8009  ixpiunwdom  8020  hsmexlem2  8810  ac6num  8862  ac6c4  8864  iundom2g  8918  seqof2  12147  rlimcld2  13383  nfsum1  13494  sumeq2ii  13497  summolem3  13518  summolem2a  13519  zsum  13522  fsum  13524  sumss2  13530  fsumcvg2  13531  fsumzcl2  13542  sumsn  13545  sumsns  13547  fsummsnunz  13551  fsumsplitsnun  13552  fsum2dlem  13567  fsumcom2  13571  fsumshftm  13578  fsum0diag2  13580  fsum00  13594  fsumabs  13597  fsumrlim  13607  fsumo1  13608  o1fsum  13609  fsumiun  13617  infcvgaux1i  13650  nfcprod1  13699  prodeq2ii  13702  prodmolem3  13722  prodmolem2a  13723  zprod  13726  fprod  13730  fprodntriv  13731  prodss  13736  fprodser  13738  prodsn  13749  fprodm1s  13756  fprodp1s  13757  prodsns  13758  fprodabs  13760  fprodn0  13765  fprod2dlem  13766  fprodcom2  13770  fprodefsum  13812  pcmpt  14393  pcmptdvds  14395  natpropd  15324  fucpropd  15325  gsummpt1n0  16971  gsumcom2  16982  gsummptnn0fz  16993  dprd2d2  17072  psrass1lem  18008  mpfrcl  18166  coe1fzgsumdlem  18322  gsummoncoe1  18325  gsumply1eq  18326  evl1gsumdlem  18371  mdetralt2  19089  mdetunilem2  19093  madugsum  19123  fiuncmp  19882  ptcld  20092  ptcldmpt  20093  ptclsg  20094  elmptrab  20306  prdsdsf  20848  prdsxmet  20850  fsumcn  21352  fsum2cn  21353  ovolfiniun  21890  ovoliunlem3  21893  ovoliun  21894  ovoliun2  21895  ovoliunnul  21896  finiunmbl  21932  volfiniun  21935  iundisj  21936  iundisj2  21937  iunmbl  21941  iunmbl2  21945  itgss3  22199  itgfsum  22211  itgabs  22219  limciun  22276  dvmptfsum  22354  dvfsumle  22400  dvfsumabs  22402  dvfsumlem1  22405  dvfsumlem2  22406  dvfsumlem3  22407  dvfsumlem4  22408  dvfsumrlim  22410  dvfsumrlim2  22411  dvfsum2  22413  itgsubstlem  22427  itgsubst  22428  rlimcnp2  23274  fsumdvdscom  23439  fsumdvdsmul  23449  fsumvma  23466  dchrisumlema  23651  dchrisumlem2  23653  dchrisumlem3  23654  disjorsf  27419  disjabrex  27421  disjabrexf  27422  iundisjf  27426  iundisj2f  27427  disjunsn  27431  suppss2f  27455  fmptdF  27473  resmptf  27475  fvmpt2f  27476  fmptcof2  27480  funcnv4mpt  27490  f1od2  27525  iundisjfi  27579  iundisj2fi  27580  gsummpt2co  27749  gsumvsca1  27751  gsumvsca2  27752  esumpfinvalf  28060  measiun  28167  voliune  28179  volfiniune  28180  sbcaltop  29607  finixpnum  30014  ptrest  30024  mbfposadd  30038  itgabsnc  30060  ftc1cnnclem  30064  ftc2nc  30075  mzpsubst  30657  rabdiophlem2  30711  elnn0rabdioph  30712  dvdsrabdioph  30719  fphpd  30726  monotuz  30853  oddcomabszz  30856  wdom2d2  30953  aomclem6  30981  flcidc  31099  fsumcnf  31350  sumsnd  31355  elabrexg  31384  fsumclf  31521  fsumsplitf  31522  fsummulc1f  31523  sumsnf  31524  fsumnncl  31526  prodsnf  31541  fproddivf  31542  fprodsplitf  31543  fprodcllemf  31545  fprodexp  31554  fprodabs2  31556  fprodle  31558  mccllem  31559  fprodcncf  31658  dvmptmulf  31688  dvnmptdivc  31689  dvmptfprod  31696  iblsplitf  31723  fourierdlem86  31929  fourierdlem112  31955  csbafv12g  32176  csbaovg  32219  fsummsndifre  32299  fsumsplitsndif  32300  fsummmodsndifre  32301  fsummmodsnunz  32302  opeliun2xp  32790  dmmpt2ssx2  32794  bj-sbeqALT  34350  fsumshftd  34557  fsumshftdOLD  34558  riotasv2s  34564  cdleme31sn  35981  cdleme31sn1  35982  cdleme31se2  35984  cdleme32fva  36038  cdleme42b  36079  hlhilset  37539
  Copyright terms: Public domain W3C validator