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

Theorem nfcsb1v 3514
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 𝑥𝐴 / 𝑥𝐵
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfcsb1v
StepHypRef Expression
1 nfcv 2750 . 2 𝑥𝐴
21nfcsb1 3513 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wnfc 2737  csb 3498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-sbc 3402  df-csb 3499
This theorem is referenced by:  csbhypf  3517  csbiebt  3518  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  sbcnestgf  3946  csbnest1g  3952  csbun  3960  csbin  3961  csbif  4087  disjors  4562  invdisjrab  4566  disjxiun  4573  disjxiunOLD  4574  disjxun  4575  sbcbr123  4630  eusvnf  4781  reusv2lem4  4792  reusv2  4794  moop2  4884  pofun  4964  opeliunxp  5082  elrnmpt1  5281  csbima12  5388  fvmpt2f  6176  fvmpts  6178  fvmpt2i  6183  fvmptex  6187  fmptco  6287  fmptcof  6288  fmptcos  6289  elabrex  6382  fliftfuns  6441  csbov123  6562  ovmpt2s  6659  ofmpteq  6791  mpt2mptsx  7099  dmmpt2ssx  7101  fmpt2x  7102  el2mpt2csbcl  7114  offval22  7117  ovmptss  7122  fmpt2co  7124  dfmpt2  7131  mpt2xeldm  7201  mpt2curryd  7259  mpt2curryvald  7260  fvmpt2curryd  7261  eqerlem  7640  qliftfuns  7698  mptelixpg  7808  boxcutc  7814  xpf1o  7984  iunfi  8114  wdom2d  8345  ixpiunwdom  8356  hsmexlem2  9109  ac6num  9161  ac6c4  9163  iundom2g  9218  seqof2  12678  rlimcld2  14105  nfsum1  14216  sumeq2ii  14219  summolem3  14240  summolem2a  14241  zsum  14244  fsum  14246  sumss2  14252  fsumcvg2  14253  fsumzcl2  14264  sumsn  14267  sumsns  14271  fsummsnunz  14275  fsumsplitsnun  14276  fsum2dlem  14291  fsumcom2  14295  fsumcom2OLD  14296  fsumshftm  14303  fsum0diag2  14305  fsum00  14319  fsumabs  14322  fsumrlim  14332  fsumo1  14333  o1fsum  14334  fsumiun  14342  infcvgaux1i  14376  nfcprod1  14427  prodeq2ii  14430  prodmolem3  14450  prodmolem2a  14451  zprod  14454  fprod  14458  fprodntriv  14459  prodss  14464  fprodser  14466  fprodcllemf  14475  prodsn  14479  prodsnf  14481  fprodm1s  14487  fprodp1s  14488  prodsns  14489  fprodabs  14491  fprodn0  14496  fprod2dlem  14497  fprodcom2  14501  fprodcom2OLD  14502  fproddivf  14505  fprodsplitf  14506  fprodle  14514  fprodmodd  14515  fprodefsum  14612  sumeven  14896  sumodd  14897  pcmpt  15382  pcmptdvds  15384  natpropd  16407  fucpropd  16408  gsummpt1n0  18135  gsumcom2  18145  gsummptnn0fz  18153  dprd2d2  18214  psrass1lem  19146  mpfrcl  19287  coe1fzgsumdlem  19440  gsummoncoe1  19443  gsumply1eq  19444  evl1gsumdlem  19489  mdetralt2  20181  mdetunilem2  20185  madugsum  20215  fiuncmp  20964  ptcld  21173  ptcldmpt  21174  ptclsg  21175  elmptrab  21387  prdsdsf  21929  prdsxmet  21931  fsumcn  22428  fsum2cn  22429  ovolfiniun  23020  ovoliunlem3  23023  ovoliun  23024  ovoliun2  23025  ovoliunnul  23026  finiunmbl  23063  volfiniun  23066  iundisj  23067  iundisj2  23068  iunmbl  23072  iunmbl2  23076  itgss3  23331  itgfsum  23343  itgabs  23351  limciun  23408  dvmptfsum  23486  dvfsumle  23532  dvfsumabs  23534  dvfsumlem1  23537  dvfsumlem2  23538  dvfsumlem3  23539  dvfsumlem4  23540  dvfsumrlim  23542  dvfsumrlim2  23543  dvfsum2  23545  itgsubstlem  23559  itgsubst  23560  rlimcnp2  24437  fsumdvdscom  24655  fsumdvdsmul  24665  fsumvma  24682  dchrisumlema  24921  dchrisumlem2  24923  dchrisumlem3  24924  disjorsf  28568  disjabrex  28570  disjabrexf  28571  iundisjf  28577  iundisj2f  28578  disjunsn  28582  suppss2f  28612  fmptdF  28629  resmptf  28631  fmptcof2  28632  acunirnmpt2f  28636  aciunf1lem  28637  funcnv4mpt  28646  f1od2  28680  iundisjfi  28735  iundisj2fi  28736  gsummpt2co  28904  gsumvsca1  28906  gsumvsca2  28907  esumpfinvalf  29258  esum2dlem  29274  esumiun  29276  fiunelros  29357  measiun  29401  voliune  29412  volfiniune  29413  sbcaltop  31051  bj-sbeqALT  31870  csbdif  32130  phpreu  32346  finixpnum  32347  ptrest  32361  poimirlem23  32385  poimirlem24  32386  poimirlem25  32387  poimirlem26  32388  poimirlem27  32389  poimirlem28  32390  mbfposadd  32410  itgabsnc  32432  ftc1cnnclem  32436  ftc2nc  32447  fsumshftd  33038  fsumshftdOLD  33039  riotasv2s  33045  cdleme31sn  34469  cdleme31sn1  34470  cdleme31se2  34472  cdleme32fva  34526  cdleme42b  34567  hlhilset  36027  mzpsubst  36112  rabdiophlem2  36167  elnn0rabdioph  36168  dvdsrabdioph  36175  fphpd  36181  monotuz  36307  oddcomabszz  36310  wdom2d2  36403  aomclem6  36430  flcidc  36546  csbcog  36743  csbingOLD  37859  fsumcnf  37986  sumsnd  37991  elabrexg  38012  fiiuncl  38042  eliin2f  38099  disjf1  38147  disjrnmpt2  38153  disjinfi  38158  iuneqfzuzlem  38274  fsumclf  38416  fsumsplitf  38417  fsummulc1f  38418  sumsnf  38419  fsumnncl  38421  fsumf1of  38424  fsumiunss  38425  fsumreclf  38426  fsumlessf  38427  fprodexp  38444  fprodabs2  38445  mccllem  38447  fprodcnlem  38449  fprodcn  38450  climeldmeqmpt  38518  fprodcncf  38570  dvmptmulf  38610  dvnmptdivc  38611  dvmptfprod  38618  iblsplitf  38645  fourierdlem86  38868  fourierdlem112  38894  sge0iunmptlemfi  39089  sge0iunmptlemre  39091  sge0iunmpt  39094  sge0ltfirpmpt2  39102  sge0isummpt2  39108  sge0xaddlem2  39110  sge0xadd  39111  hoimbl2  39338  vonn0ioo2  39364  vonn0icc2  39366  csbafv12g  39650  csbaovg  39693  iunopeqop  40110  fsummsndifre  40200  fsumsplitsndif  40201  fsummmodsndifre  40202  fsummmodsnunz  40203  rspc2vd  41418  opeliun2xp  41885  dmmpt2ssx2  41889
  Copyright terms: Public domain W3C validator