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

Theorem nfcsb1v 3417
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 2591 . 2  |-  F/_ x A
21nfcsb1 3416 1  |-  F/_ x [_ A  /  x ]_ B
Colors of variables: wff setvar class
Syntax hints:   F/_wnfc 2577   [_csb 3401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-sbc 3306  df-csb 3402
This theorem is referenced by:  csbhypf  3420  csbiebt  3421  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  sbcnestgf  3818  csbnest1g  3824  csbun  3832  csbin  3833  csbif  3965  csbopg  4208  disjors  4412  invdisjrab  4416  disjxiun  4423  disjxun  4424  sbcbr123  4477  eusvnf  4620  reusv2lem4  4629  reusv2  4631  moop2  4716  pofun  4791  opeliunxp  4906  elrnmpt1  5103  csbima12  5205  csbima12gOLD  5206  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  mpt2curryd  7024  mpt2curryvald  7025  fvmpt2curryd  7026  eqerlem  7403  qliftfuns  7458  mptelixpg  7567  boxcutc  7573  xpf1o  7740  iunfi  7868  wdom2d  8095  ixpiunwdom  8106  hsmexlem2  8855  ac6num  8907  ac6c4  8909  iundom2g  8963  seqof2  12268  rlimcld2  13620  nfsum1  13734  sumeq2ii  13737  summolem3  13758  summolem2a  13759  zsum  13762  fsum  13764  sumss2  13770  fsumcvg2  13771  fsumzcl2  13782  sumsn  13785  sumsns  13789  fsummsnunz  13793  fsumsplitsnun  13794  fsum2dlem  13809  fsumcom2  13813  fsumshftm  13820  fsum0diag2  13822  fsum00  13836  fsumabs  13839  fsumrlim  13849  fsumo1  13850  o1fsum  13851  fsumiun  13859  infcvgaux1i  13893  nfcprod1  13942  prodeq2ii  13945  prodmolem3  13965  prodmolem2a  13966  zprod  13969  fprod  13973  fprodntriv  13974  prodss  13979  fprodser  13981  fprodcllemf  13990  prodsn  13994  prodsnf  13996  fprodm1s  14002  fprodp1s  14003  prodsns  14004  fprodabs  14006  fprodn0  14011  fprod2dlem  14012  fprodcom2  14016  fproddivf  14019  fprodsplitf  14020  fprodle  14028  fprodefsum  14127  pcmpt  14800  pcmptdvds  14802  natpropd  15832  fucpropd  15833  gsummpt1n0  17532  gsumcom2  17542  gsummptnn0fz  17550  dprd2d2  17612  psrass1lem  18536  mpfrcl  18676  coe1fzgsumdlem  18830  gsummoncoe1  18833  gsumply1eq  18834  evl1gsumdlem  18879  mdetralt2  19565  mdetunilem2  19569  madugsum  19599  fiuncmp  20350  ptcld  20559  ptcldmpt  20560  ptclsg  20561  elmptrab  20773  prdsdsf  21313  prdsxmet  21315  fsumcn  21798  fsum2cn  21799  ovolfiniun  22332  ovoliunlem3  22335  ovoliun  22336  ovoliun2  22337  ovoliunnul  22338  finiunmbl  22374  volfiniun  22377  iundisj  22378  iundisj2  22379  iunmbl  22383  iunmbl2  22387  itgss3  22649  itgfsum  22661  itgabs  22669  limciun  22726  dvmptfsum  22804  dvfsumle  22850  dvfsumabs  22852  dvfsumlem1  22855  dvfsumlem2  22856  dvfsumlem3  22857  dvfsumlem4  22858  dvfsumrlim  22860  dvfsumrlim2  22861  dvfsum2  22863  itgsubstlem  22877  itgsubst  22878  rlimcnp2  23757  fsumdvdscom  23977  fsumdvdsmul  23987  fsumvma  24004  dchrisumlema  24189  dchrisumlem2  24191  dchrisumlem3  24192  disjorsf  28029  disjabrex  28031  disjabrexf  28032  iundisjf  28038  iundisj2f  28039  disjunsn  28043  suppss2fOLD  28077  suppss2f  28078  fmptdF  28095  resmptf  28097  fmptcof2  28099  acunirnmpt2f  28103  aciunf1lem  28104  funcnv4mpt  28113  f1od2  28152  iundisjfi  28208  iundisj2fi  28209  gsummpt2co  28381  gsumvsca1  28384  gsumvsca2  28385  esumpfinvalf  28736  esum2dlem  28752  esumiun  28754  fiunelros  28835  measiun  28879  voliune  28891  volfiniune  28892  sbcaltop  30533  bj-sbeqALT  31252  csbdif  31470  phpreu  31632  finixpnum  31633  ptrest  31642  poimirlem23  31666  poimirlem24  31667  poimirlem25  31668  poimirlem26  31669  poimirlem27  31670  poimirlem28  31671  mbfposadd  31691  itgabsnc  31714  ftc1cnnclem  31718  ftc2nc  31729  fsumshftd  32231  fsumshftdOLD  32232  riotasv2s  32238  cdleme31sn  33655  cdleme31sn1  33656  cdleme31se2  33658  cdleme32fva  33712  cdleme42b  33753  hlhilset  35213  mzpsubst  35298  rabdiophlem2  35353  elnn0rabdioph  35354  dvdsrabdioph  35361  fphpd  35367  monotuz  35494  oddcomabszz  35497  wdom2d2  35595  aomclem6  35622  flcidc  35738  csbcog  35879  csbingOLD  36854  fsumcnf  36981  sumsnd  36986  elabrexg  37009  fiiuncl  37047  disjf1  37079  disjrnmpt2  37085  disjinfi  37090  iuneqfzuzlem  37165  fsumclf  37219  fsumsplitf  37220  fsummulc1f  37221  sumsnf  37222  fsumnncl  37224  fsumf1of  37227  fsumiunss  37228  fprodexp  37245  fprodabs2  37246  mccllem  37248  fprodcncf  37350  dvmptmulf  37380  dvnmptdivc  37381  dvmptfprod  37388  iblsplitf  37415  fourierdlem86  37623  fourierdlem112  37649  sge0iunmptlemfi  37788  sge0iunmptlemre  37790  sge0iunmpt  37793  csbafv12g  38028  csbaovg  38071  fsummsndifre  38414  fsumsplitsndif  38415  fsummmodsndifre  38416  fsummmodsnunz  38417  opeliun2xp  38873  dmmpt2ssx2  38877
  Copyright terms: Public domain W3C validator