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

Theorem nfcsb1v 3706
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 2906 . 2 𝑥𝐴
21nfcsb1 3705 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wnfc 2893  csb 3690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-sbc 3596  df-csb 3691
This theorem is referenced by:  csbhypf  3709  csbiebt  3710  cbvralcsf  3722  cbvreucsf  3724  cbvrabcsf  3725  sbcnestgf  4155  csbnest1g  4161  csbun  4170  csbin  4171  csbif  4297  disjors  4791  invdisjrab  4795  disjxiun  4805  disjxun  4806  sbcbr123  4862  eusvnf  5026  reusv2lem4  5035  reusv2  5037  moop2  5120  iunopeqop  5141  pofun  5213  opeliunxp  5337  elrnmpt1  5542  resmptf  5627  csbima12  5664  fvmpt2f  6471  fvmpts  6473  fvmpt2i  6478  fvmptex  6482  fmptco  6586  fmptcof  6587  fmptcos  6588  elabrex  6692  fliftfuns  6755  csbov123  6882  ovmpt2s  6981  ofmpteq  7113  mpt2mptsx  7433  dmmpt2ssx  7435  fmpt2x  7436  el2mpt2csbcl  7450  offval22  7454  ovmptss  7459  fmpt2co  7461  dfmpt2  7468  mpt2xeldm  7539  mpt2curryd  7597  mpt2curryvald  7598  fvmpt2curryd  7599  eqerlem  7980  qliftfuns  8036  mptelixpg  8149  boxcutc  8155  xpf1o  8328  iunfi  8460  wdom2d  8691  ixpiunwdom  8702  hsmexlem2  9501  ac6num  9553  ac6c4  9555  iundom2g  9614  seqof2  13065  rlimcld2  14595  nfsum1  14706  sumeq2ii  14709  summolem3  14731  summolem2a  14732  zsum  14735  fsum  14737  sumss2  14743  fsumcvg2  14744  fsumzcl2  14755  fsumsplitf  14758  sumsnf  14759  sumsns  14765  fsummsnunz  14769  fsumsplitsnun  14770  fsummsnunzOLD  14771  fsumsplitsnunOLD  14772  fsum2dlem  14787  fsumcom2  14791  fsumshftm  14798  fsum0diag2  14800  fsum00  14815  fsumabs  14818  fsumrlim  14828  fsumo1  14829  o1fsum  14830  fsumiun  14838  infcvgaux1i  14874  nfcprod1  14924  prodeq2ii  14927  prodmolem3  14947  prodmolem2a  14948  zprod  14951  fprod  14955  fprodntriv  14956  prodss  14961  fprodser  14963  fprodcllemf  14972  prodsn  14976  prodsnf  14978  fprodm1s  14984  fprodp1s  14985  prodsns  14986  fprodabs  14988  fprodn0  14993  fprod2dlem  14994  fprodcom2  14998  fproddivf  15001  fprodsplitf  15002  fprodle  15010  fprodmodd  15011  fprodefsum  15108  sumeven  15393  sumodd  15394  pcmpt  15876  pcmptdvds  15878  natpropd  16902  fucpropd  16903  gsummpt1n0  18629  gsumcom2  18639  gsummptnn0fz  18647  gsummptnn0fzOLD  18648  dprd2d2  18709  psrass1lem  19650  mpfrcl  19790  coe1fzgsumdlem  19943  gsummoncoe1  19946  gsumply1eq  19947  evl1gsumdlem  19992  mdetralt2  20691  mdetunilem2  20695  madugsum  20725  fiuncmp  21486  ptcld  21695  ptcldmpt  21696  ptclsg  21697  elmptrab  21909  prdsdsf  22450  prdsxmet  22452  fsumcn  22951  fsum2cn  22952  ovolfiniun  23558  ovoliunlem3  23561  ovoliun  23562  ovoliun2  23563  ovoliunnul  23564  finiunmbl  23601  volfiniun  23604  iundisj  23605  iundisj2  23606  iunmbl  23610  iunmbl2  23614  itgss3  23871  itgfsum  23883  itgabs  23891  limciun  23948  dvmptfsum  24028  dvfsumle  24074  dvfsumabs  24076  dvfsumlem1  24079  dvfsumlem2  24080  dvfsumlem3  24081  dvfsumlem4  24082  dvfsumrlim  24084  dvfsumrlim2  24085  dvfsum2  24087  itgsubstlem  24101  itgsubst  24102  rlimcnp2  24983  fsumdvdscom  25201  fsumdvdsmul  25211  fsumvma  25228  dchrisumlema  25467  dchrisumlem2  25469  dchrisumlem3  25470  rspc2vd  27502  disjorsf  29775  disjabrex  29777  disjabrexf  29778  iundisjf  29784  iundisj2f  29785  disjunsn  29789  suppss2f  29823  fmptdF  29840  fmptcof2  29841  acunirnmpt2f  29845  aciunf1lem  29846  funcnv4mpt  29853  f1od2  29882  iundisjfi  29938  iundisj2fi  29939  fsumiunle  29958  gsummpt2co  30161  gsumvsca1  30163  gsumvsca2  30164  esumpfinvalf  30519  esum2dlem  30535  esumiun  30537  fiunelros  30618  measiun  30662  voliune  30673  volfiniune  30674  sbcaltop  32463  bj-sbeqALT  33252  csbdif  33537  phpreu  33749  finixpnum  33750  ptrest  33764  poimirlem23  33788  poimirlem24  33789  poimirlem25  33790  poimirlem26  33791  poimirlem27  33792  poimirlem28  33793  mbfposadd  33812  itgabsnc  33834  ftc1cnnclem  33838  ftc2nc  33849  fsumshftd  34840  riotasv2s  34846  cdleme31sn  36268  cdleme31sn1  36269  cdleme31se2  36271  cdleme32fva  36325  cdleme42b  36366  hlhilset  37822  mzpsubst  37921  rabdiophlem2  37976  elnn0rabdioph  37977  dvdsrabdioph  37984  fphpd  37990  monotuz  38115  oddcomabszz  38118  wdom2d2  38211  aomclem6  38238  flcidc  38353  csbcog  38548  fsumcnf  39764  sumsnd  39769  elabrexg  39790  fiiuncl  39817  eliin2f  39869  disjf1  39948  disjrnmpt2  39954  disjinfi  39959  fmptf  40022  iuneqfzuzlem  40120  supxrleubrnmptf  40249  fsumclf  40371  fsummulc1f  40372  fsumnncl  40373  fsumf1of  40376  fsumiunss  40377  fsumreclf  40378  fsumlessf  40379  fprodexp  40396  fprodabs2  40397  mccllem  40399  fprodcnlem  40401  fprodcn  40402  climeldmeqmpt  40470  climeldmeqmpt3  40491  climinf2mpt  40516  climinfmpt  40517  limsupequzmptf  40533  fprodcncf  40684  dvmptmulf  40722  dvnmptdivc  40723  dvmptfprod  40730  iblsplitf  40755  fourierdlem86  40978  fourierdlem112  41004  sge0iunmptlemfi  41199  sge0iunmptlemre  41201  sge0iunmpt  41204  sge0ltfirpmpt2  41212  sge0isummpt2  41218  sge0xaddlem2  41220  sge0xadd  41221  hoimbl2  41451  vonn0ioo2  41476  vonn0icc2  41478  csbafv12g  41817  csbaovg  41860  csbafv212g  41899  fsummsndifre  42008  fsumsplitsndif  42009  fsummmodsndifre  42010  fsummmodsnunz  42011  opeliun2xp  42712  dmmpt2ssx2  42716
  Copyright terms: Public domain W3C validator