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

Theorem nfcsb1v 3411
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 2580 . 2  |-  F/_ x A
21nfcsb1 3410 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2566   [_csb 3395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-sbc 3300  df-csb 3396
This theorem is referenced by:  csbhypf  3414  csbiebt  3415  cbvralcsf  3427  cbvreucsf  3429  cbvrabcsf  3430  sbcnestgf  3814  csbnest1g  3820  csbun  3828  csbin  3829  csbif  3961  csbopg  4205  disjors  4409  invdisjrab  4413  disjxiun  4420  disjxun  4421  sbcbr123  4475  eusvnf  4619  reusv2lem4  4628  reusv2  4630  moop2  4715  pofun  4790  opeliunxp  4905  elrnmpt1  5102  csbima12  5204  csbima12gOLD  5205  fvmpt2f  5965  fvmpts  5967  fvmpt2i  5972  fvmptex  5976  fmptco  6071  fmptcof  6072  fmptcos  6073  elabrex  6163  fliftfuns  6222  csbov123  6339  ovmpt2s  6434  ofmpteq  6564  mpt2mptsx  6870  dmmpt2ssx  6872  fmpt2x  6873  offval22  6886  ovmptss  6888  fmpt2co  6890  dfmpt2  6897  mpt2xeldm  6968  mpt2curryd  7027  mpt2curryvald  7028  fvmpt2curryd  7029  eqerlem  7406  qliftfuns  7461  mptelixpg  7570  boxcutc  7576  xpf1o  7743  iunfi  7871  wdom2d  8104  ixpiunwdom  8115  hsmexlem2  8864  ac6num  8916  ac6c4  8918  iundom2g  8972  seqof2  12277  rlimcld2  13641  nfsum1  13755  sumeq2ii  13758  summolem3  13779  summolem2a  13780  zsum  13783  fsum  13785  sumss2  13791  fsumcvg2  13792  fsumzcl2  13803  sumsn  13806  sumsns  13810  fsummsnunz  13814  fsumsplitsnun  13815  fsum2dlem  13830  fsumcom2  13834  fsumshftm  13841  fsum0diag2  13843  fsum00  13857  fsumabs  13860  fsumrlim  13870  fsumo1  13871  o1fsum  13872  fsumiun  13880  infcvgaux1i  13914  nfcprod1  13963  prodeq2ii  13966  prodmolem3  13986  prodmolem2a  13987  zprod  13990  fprod  13994  fprodntriv  13995  prodss  14000  fprodser  14002  fprodcllemf  14011  prodsn  14015  prodsnf  14017  fprodm1s  14023  fprodp1s  14024  prodsns  14025  fprodabs  14027  fprodn0  14032  fprod2dlem  14033  fprodcom2  14037  fproddivf  14040  fprodsplitf  14041  fprodle  14049  fprodefsum  14148  pcmpt  14836  pcmptdvds  14838  natpropd  15880  fucpropd  15881  gsummpt1n0  17596  gsumcom2  17606  gsummptnn0fz  17614  dprd2d2  17676  psrass1lem  18600  mpfrcl  18740  coe1fzgsumdlem  18894  gsummoncoe1  18897  gsumply1eq  18898  evl1gsumdlem  18943  mdetralt2  19632  mdetunilem2  19636  madugsum  19666  fiuncmp  20417  ptcld  20626  ptcldmpt  20627  ptclsg  20628  elmptrab  20840  prdsdsf  21380  prdsxmet  21382  fsumcn  21900  fsum2cn  21901  ovolfiniun  22452  ovoliunlem3  22455  ovoliun  22456  ovoliun2  22457  ovoliunnul  22458  finiunmbl  22495  volfiniun  22498  iundisj  22499  iundisj2  22500  iunmbl  22504  iunmbl2  22508  itgss3  22770  itgfsum  22782  itgabs  22790  limciun  22847  dvmptfsum  22925  dvfsumle  22971  dvfsumabs  22973  dvfsumlem1  22976  dvfsumlem2  22977  dvfsumlem3  22978  dvfsumlem4  22979  dvfsumrlim  22981  dvfsumrlim2  22982  dvfsum2  22984  itgsubstlem  22998  itgsubst  22999  rlimcnp2  23890  fsumdvdscom  24112  fsumdvdsmul  24122  fsumvma  24139  dchrisumlema  24324  dchrisumlem2  24326  dchrisumlem3  24327  disjorsf  28192  disjabrex  28194  disjabrexf  28195  iundisjf  28201  iundisj2f  28202  disjunsn  28206  suppss2fOLD  28239  suppss2f  28240  fmptdF  28257  resmptf  28259  fmptcof2  28261  acunirnmpt2f  28265  aciunf1lem  28266  funcnv4mpt  28275  f1od2  28315  iundisjfi  28378  iundisj2fi  28379  gsummpt2co  28550  gsumvsca1  28553  gsumvsca2  28554  esumpfinvalf  28905  esum2dlem  28921  esumiun  28923  fiunelros  29004  measiun  29048  voliune  29060  volfiniune  29061  sbcaltop  30753  bj-sbeqALT  31471  csbdif  31690  phpreu  31893  finixpnum  31894  ptrest  31903  poimirlem23  31927  poimirlem24  31928  poimirlem25  31929  poimirlem26  31930  poimirlem27  31931  poimirlem28  31932  mbfposadd  31952  itgabsnc  31975  ftc1cnnclem  31979  ftc2nc  31990  fsumshftd  32492  fsumshftdOLD  32493  riotasv2s  32499  cdleme31sn  33916  cdleme31sn1  33917  cdleme31se2  33919  cdleme32fva  33973  cdleme42b  34014  hlhilset  35474  mzpsubst  35559  rabdiophlem2  35614  elnn0rabdioph  35615  dvdsrabdioph  35622  fphpd  35628  monotuz  35759  oddcomabszz  35762  wdom2d2  35860  aomclem6  35887  flcidc  36010  csbcog  36211  csbingOLD  37188  fsumcnf  37315  sumsnd  37320  elabrexg  37343  fiiuncl  37379  disjf1  37418  disjrnmpt2  37424  disjinfi  37429  iuneqfzuzlem  37511  fsumclf  37586  fsumsplitf  37587  fsummulc1f  37588  sumsnf  37589  fsumnncl  37591  fsumf1of  37594  fsumiunss  37595  fsumreclf  37596  fsumlessf  37597  fprodexp  37614  fprodabs2  37615  mccllem  37617  fprodcncf  37719  dvmptmulf  37752  dvnmptdivc  37753  dvmptfprod  37760  iblsplitf  37787  fourierdlem86  37996  fourierdlem112  38022  sge0iunmptlemfi  38163  sge0iunmptlemre  38165  sge0iunmpt  38168  sge0ltfirpmpt2  38176  sge0isummpt2  38182  sge0xaddlem2  38184  sge0xadd  38185  csbafv12g  38509  csbaovg  38552  iunopeqop  38870  fsummsndifre  38921  fsumsplitsndif  38922  fsummmodsndifre  38923  fsummmodsnunz  38924  opeliun2xp  39736  dmmpt2ssx2  39740
  Copyright terms: Public domain W3C validator