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

Theorem cbvrexv 3202
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrexv (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrexv
StepHypRef Expression
1 nfv 1883 . 2 𝑦𝜑
2 nfv 1883 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvrex 3198 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947
This theorem is referenced by:  cbvrex2v  3210  reu7  3434  disjiund  4675  reusv3  4906  xpdifid  5597  fliftfun  6602  grpridd  6916  funcnvuni  7161  fun11iun  7168  nneob  7777  pssnn  8219  frfi  8246  finsschain  8314  marypha1lem  8380  supmo  8399  suplub2  8408  infmo  8442  ordtypelem3  8466  ordtypelem9  8472  wemaplem1  8492  brwdom3  8528  unwdomg  8530  cantnf  8628  trcl  8642  infxpenc2  8883  aceq2  8980  dfac5lem4  8987  kmlem9  9018  kmlem14  9023  fin23lem26  9185  fin1a2lem13  9272  axdc3lem3  9312  winainflem  9553  axgroth4  9692  suprlub  11025  supaddc  11028  supadd  11029  supmul1  11030  supmullem1  11031  supmullem2  11032  supmul  11033  ublbneg  11811  zsupss  11815  xrsupsslem  12175  xrinfmsslem  12176  fsuppmapnn0fiubOLD  12831  rexanre  14130  rexuzre  14136  rexico  14137  caurcvg2  14452  caucvgb  14454  summolem2  14491  summo  14492  mertens  14662  prodmolem2  14709  prodmo  14710  odd2np1lem  15111  gcdcllem1  15268  pceu  15598  4sqlem12  15707  vdwlem10  15741  vdwlem13  15744  vdwnn  15749  drsdirfi  16985  dfgrp2  17494  dfgrp3lem  17560  gaorb  17786  psgnunilem3  17962  psgnunilem4  17963  psgneu  17972  pj1eu  18155  efgsfo  18198  cyggeninv  18331  cygabl  18338  pgpfac1lem5  18524  pgpfac1  18525  pgpfaclem2  18527  lss1d  19011  lspsneq  19170  lspsolvlem  19190  lbsextlem2  19207  mplcoe5lem  19515  cygznlem3  19966  pmatcollpw3fi1lem2  20640  ordtrest2lem  21055  cnprest  21141  1stcfb  21296  1stcelcls  21312  elpt  21423  fbssfi  21688  fgcl  21729  rnelfmlem  21803  fmfnfmlem3  21807  txflf  21857  alexsubb  21897  alexsubALTlem4  21901  isucn2  22130  icccmplem2  22673  ply1divex  23941  coeeu  24026  plydivex  24097  aannenlem2  24129  ulmcau  24194  ulmbdd  24197  dchrptlem2  25035  bposlem9  25062  2lgslem1b  25162  pntibndlem3  25326  pntlemi  25338  pntlemp  25344  pntleml  25345  pnt3  25346  legval  25524  legov  25525  legov2  25526  outpasch  25692  lnopp2hpgb  25700  colopp  25706  erclwwlksym  26978  erclwwlktr  26979  erclwwlknsym  27034  erclwwlkntr  27035  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  grpoidinvlem3  27488  ubthlem3  27856  norm1exi  28235  pjhthmo  28289  cdjreui  29419  cdj3i  29428  infxrge0glb  29658  isarchi3  29869  archiabl  29880  ordtrest2NEWlem  30096  lmxrge0  30126  esumcvg  30276  esum2d  30283  eulerpartlems  30550  eulerpartlemgvv  30566  connpconn  31343  cvmlift2lem12  31422  cvmlift2lem13  31423  cvmlift3lem2  31428  cvmlift3lem7  31433  cvmlift3  31436  poseq  31878  soseq  31879  noprefixmo  31973  nosupdm  31975  nosupfv  31977  nosupres  31978  nosupbnd1lem1  31979  nosupbnd1lem4  31982  funtransport  32263  funray  32372  funline  32374  fnessref  32477  neibastop2  32481  dissneqlem  33317  dissneq  33318  ptrest  33538  poimirlem27  33566  poimirlem32  33571  ismblfin  33580  volsupnfl  33584  itg2addnclem  33591  unirep  33637  filbcmb  33665  sdclem1  33669  sdc  33670  fdc  33671  incsequz  33674  heibor1lem  33738  heiborlem10  33749  isgrpda  33884  isdrngo2  33887  prnc  33996  prtlem13  34472  prtlem15  34479  lshpsmreu  34714  lshpkrlem1  34715  lshpkrlem3  34717  pclfinN  35504  4atex  35680  dihglblem2N  36900  lcfl7N  37107  lcf1o  37157  mzpcompact2lem  37631  eldioph3  37646  diophrex  37656  rexrabdioph  37675  eldioph4i  37693  aomclem8  37948  hbtlem2  38011  rngunsnply  38060  iunrelexpuztr  38328  ntrclsneine0lem  38679  dvconstbi  38850  expgrowth  38851  wessf1ornlem  39685  rnmptlb  39767  rnmptbdd  39770  rnmptbd2  39778  rnmptbd  39785  rexabsle  39959  uzub  39971  infrpgernmpt  40008  limcperiod  40178  limsupre  40191  limsupref  40235  limsupbnd1f  40236  climinfmpt  40265  limsupubuzmpt  40269  limsupmnf  40271  limsupre2  40275  limsupmnfuzlem  40276  limsupmnfuz  40277  limsupre2mpt  40280  limsupre3  40283  limsupre3mpt  40284  limsupre3uz  40286  limsupreuz  40287  limsupreuzmpt  40289  supcnvlimsup  40290  climuz  40294  lmbr3  40297  climrescn  40298  limsuplt2  40303  liminflelimsup  40326  limsupgt  40328  liminfreuz  40353  liminflt  40355  xlimmnf  40385  xlimpnf  40386  xlimmnfmpt  40387  xlimpnfmpt  40388  dfxlim2  40392  cncfshiftioo  40423  itgiccshift  40514  itgperiod  40515  fourierdlem42  40684  fourierdlem48  40689  fourierdlem81  40722  fourierdlem92  40733  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem105  40746  fourierdlem108  40749  fourierdlem110  40751  fourierdlem112  40753  fourierdlem113  40754  meaiuninc3v  41019  hoidmvval0  41122  ovnhoi  41138  ovolval5lem3  41189  ovolval5  41190  smfsup  41341  smfinflem  41344  smfinf  41345  fmtnofac2lem  41805  2zlidl  42259  2zrngamgm  42264  2zrngagrp  42268  2zrngmmgm  42271
  Copyright terms: Public domain W3C validator