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

Theorem nfcsb1v 3515
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 2751 . 2 𝑥𝐴
21nfcsb1 3514 1 𝑥𝐴 / 𝑥𝐵
Colors of variables: wff setvar class
Syntax hints:  wnfc 2738  csb 3499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-sbc 3403  df-csb 3500
This theorem is referenced by:  csbhypf  3518  csbiebt  3519  cbvralcsf  3531  cbvreucsf  3533  cbvrabcsf  3534  sbcnestgf  3947  csbnest1g  3953  csbun  3961  csbin  3962  csbif  4088  disjors  4568  invdisjrab  4572  disjxiun  4579  disjxiunOLD  4580  disjxun  4581  sbcbr123  4636  eusvnf  4787  reusv2lem4  4798  reusv2  4800  moop2  4891  iunopeqop  4906  pofun  4975  opeliunxp  5093  elrnmpt1  5295  csbima12  5402  fvmpt2f  6192  fvmpts  6194  fvmpt2i  6199  fvmptex  6203  fmptco  6303  fmptcof  6304  fmptcos  6305  elabrex  6405  fliftfuns  6464  csbov123  6585  ovmpt2s  6682  ofmpteq  6814  mpt2mptsx  7122  dmmpt2ssx  7124  fmpt2x  7125  el2mpt2csbcl  7137  offval22  7140  ovmptss  7145  fmpt2co  7147  dfmpt2  7154  mpt2xeldm  7224  mpt2curryd  7282  mpt2curryvald  7283  fvmpt2curryd  7284  eqerlem  7663  qliftfuns  7721  mptelixpg  7831  boxcutc  7837  xpf1o  8007  iunfi  8137  wdom2d  8368  ixpiunwdom  8379  hsmexlem2  9132  ac6num  9184  ac6c4  9186  iundom2g  9241  seqof2  12721  rlimcld2  14157  nfsum1  14268  sumeq2ii  14271  summolem3  14292  summolem2a  14293  zsum  14296  fsum  14298  sumss2  14304  fsumcvg2  14305  fsumzcl2  14316  sumsn  14319  sumsns  14323  fsummsnunz  14327  fsumsplitsnun  14328  fsum2dlem  14343  fsumcom2  14347  fsumcom2OLD  14348  fsumshftm  14355  fsum0diag2  14357  fsum00  14371  fsumabs  14374  fsumrlim  14384  fsumo1  14385  o1fsum  14386  fsumiun  14394  infcvgaux1i  14428  nfcprod1  14479  prodeq2ii  14482  prodmolem3  14502  prodmolem2a  14503  zprod  14506  fprod  14510  fprodntriv  14511  prodss  14516  fprodser  14518  fprodcllemf  14527  prodsn  14531  prodsnf  14533  fprodm1s  14539  fprodp1s  14540  prodsns  14541  fprodabs  14543  fprodn0  14548  fprod2dlem  14549  fprodcom2  14553  fprodcom2OLD  14554  fproddivf  14557  fprodsplitf  14558  fprodle  14566  fprodmodd  14567  fprodefsum  14664  sumeven  14948  sumodd  14949  pcmpt  15434  pcmptdvds  15436  natpropd  16459  fucpropd  16460  gsummpt1n0  18187  gsumcom2  18197  gsummptnn0fz  18205  dprd2d2  18266  psrass1lem  19198  mpfrcl  19339  coe1fzgsumdlem  19492  gsummoncoe1  19495  gsumply1eq  19496  evl1gsumdlem  19541  mdetralt2  20234  mdetunilem2  20238  madugsum  20268  fiuncmp  21017  ptcld  21226  ptcldmpt  21227  ptclsg  21228  elmptrab  21440  prdsdsf  21982  prdsxmet  21984  fsumcn  22481  fsum2cn  22482  ovolfiniun  23076  ovoliunlem3  23079  ovoliun  23080  ovoliun2  23081  ovoliunnul  23082  finiunmbl  23119  volfiniun  23122  iundisj  23123  iundisj2  23124  iunmbl  23128  iunmbl2  23132  itgss3  23387  itgfsum  23399  itgabs  23407  limciun  23464  dvmptfsum  23542  dvfsumle  23588  dvfsumabs  23590  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsumrlim  23598  dvfsumrlim2  23599  dvfsum2  23601  itgsubstlem  23615  itgsubst  23616  rlimcnp2  24493  fsumdvdscom  24711  fsumdvdsmul  24721  fsumvma  24738  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  disjorsf  28775  disjabrex  28777  disjabrexf  28778  iundisjf  28784  iundisj2f  28785  disjunsn  28789  suppss2f  28819  fmptdF  28836  resmptf  28838  fmptcof2  28839  acunirnmpt2f  28843  aciunf1lem  28844  funcnv4mpt  28853  f1od2  28887  iundisjfi  28942  iundisj2fi  28943  gsummpt2co  29111  gsumvsca1  29113  gsumvsca2  29114  esumpfinvalf  29465  esum2dlem  29481  esumiun  29483  fiunelros  29564  measiun  29608  voliune  29619  volfiniune  29620  sbcaltop  31258  bj-sbeqALT  32087  csbdif  32347  phpreu  32563  finixpnum  32564  ptrest  32578  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem28  32607  mbfposadd  32627  itgabsnc  32649  ftc1cnnclem  32653  ftc2nc  32664  fsumshftd  33255  fsumshftdOLD  33256  riotasv2s  33262  cdleme31sn  34686  cdleme31sn1  34687  cdleme31se2  34689  cdleme32fva  34743  cdleme42b  34784  hlhilset  36244  mzpsubst  36329  rabdiophlem2  36384  elnn0rabdioph  36385  dvdsrabdioph  36392  fphpd  36398  monotuz  36524  oddcomabszz  36527  wdom2d2  36620  aomclem6  36647  flcidc  36763  csbcog  36960  csbingOLD  38076  fsumcnf  38203  sumsnd  38208  elabrexg  38229  fiiuncl  38259  eliin2f  38316  disjf1  38364  disjrnmpt2  38370  disjinfi  38375  iuneqfzuzlem  38491  fsumclf  38633  fsumsplitf  38634  fsummulc1f  38635  sumsnf  38636  fsumnncl  38638  fsumf1of  38641  fsumiunss  38642  fsumreclf  38643  fsumlessf  38644  fprodexp  38661  fprodabs2  38662  mccllem  38664  fprodcnlem  38666  fprodcn  38667  climeldmeqmpt  38735  fprodcncf  38787  dvmptmulf  38827  dvnmptdivc  38828  dvmptfprod  38835  iblsplitf  38862  fourierdlem86  39085  fourierdlem112  39111  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0iunmpt  39311  sge0ltfirpmpt2  39319  sge0isummpt2  39325  sge0xaddlem2  39327  sge0xadd  39328  hoimbl2  39555  vonn0ioo2  39581  vonn0icc2  39583  csbafv12g  39866  csbaovg  39909  fsummsndifre  40371  fsumsplitsndif  40372  fsummmodsndifre  40373  fsummmodsnunz  40374  rspc2vd  41437  opeliun2xp  41904  dmmpt2ssx2  41908
  Copyright terms: Public domain W3C validator