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

Theorem cbvrexv 3147
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 1829 . 2 𝑦𝜑
2 nfv 1829 . 2 𝑥𝜓
3 cbvralv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvrex 3143 1 (∃𝑥𝐴 𝜑 ↔ ∃𝑦𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wrex 2896
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-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901
This theorem is referenced by:  cbvrex2v  3155  reu7  3367  reusv3  4797  xpdifid  5467  fliftfun  6440  grpridd  6749  funcnvuni  6989  fun11iun  6996  nneob  7596  pssnn  8040  frfi  8067  finsschain  8133  marypha1lem  8199  supmo  8218  suplub2  8227  infmo  8261  ordtypelem3  8285  ordtypelem9  8291  wemaplem1  8311  brwdom3  8347  unwdomg  8349  cantnf  8450  trcl  8464  infxpenc2  8705  aceq2  8802  dfac5lem4  8809  kmlem9  8840  kmlem14  8845  fin23lem26  9007  fin1a2lem13  9094  axdc3lem3  9134  winainflem  9371  axgroth4  9510  suprlub  10834  supaddc  10837  supadd  10838  supmul1  10839  supmullem1  10840  supmullem2  10841  supmul  10842  ublbneg  11605  zsupss  11609  xrsupsslem  11965  xrinfmsslem  11966  fsuppmapnn0fiubOLD  12608  rexanre  13880  rexuzre  13886  rexico  13887  caurcvg2  14202  caucvgb  14204  summolem2  14240  summo  14241  mertens  14403  prodmolem2  14450  prodmo  14451  odd2np1lem  14848  gcdcllem1  15005  pceu  15335  4sqlem12  15444  vdwlem10  15478  vdwlem13  15481  vdwnn  15486  drsdirfi  16707  dfgrp2  17216  dfgrp3lem  17282  gaorb  17509  psgnunilem3  17685  psgnunilem4  17686  psgneu  17695  pj1eu  17878  efgsfo  17921  cyggeninv  18054  cygabl  18061  pgpfac1lem5  18247  pgpfac1  18248  pgpfaclem2  18250  lss1d  18730  lspsneq  18889  lspsolvlem  18909  lbsextlem2  18926  mplcoe5lem  19234  cygznlem3  19682  pmatcollpw3fi1lem2  20353  ordtrest2lem  20759  cnprest  20845  1stcfb  21000  1stcelcls  21016  elpt  21127  fbssfi  21393  fgcl  21434  rnelfmlem  21508  fmfnfmlem3  21512  txflf  21562  alexsubb  21602  alexsubALTlem4  21606  isucn2  21835  icccmplem2  22366  ply1divex  23617  coeeu  23702  plydivex  23773  aannenlem2  23805  ulmcau  23870  ulmbdd  23873  dchrptlem2  24707  bposlem9  24734  2lgslem1b  24834  pntibndlem3  24998  pntlemi  25010  pntlemp  25016  pntleml  25017  pnt3  25018  legval  25197  legov  25198  legov2  25199  outpasch  25365  lnopp2hpgb  25373  colopp  25379  erclwwlksym  26108  erclwwlktr  26109  erclwwlknsym  26120  erclwwlkntr  26121  eleclclwwlkn  26126  hashecclwwlkn1  26127  usghashecclwwlk  26128  frgraregorufr0  26345  grpoidinvlem3  26510  ubthlem3  26918  norm1exi  27297  pjhthmo  27351  cdjreui  28481  cdj3i  28490  infxrge0glb  28726  isarchi3  28878  archiabl  28889  ordtrest2NEWlem  29102  lmxrge0  29132  esumcvg  29281  esum2d  29288  eulerpartlems  29555  eulerpartlemgvv  29571  conpcon  30277  cvmlift2lem12  30356  cvmlift2lem13  30357  cvmlift3lem2  30362  cvmlift3lem7  30367  cvmlift3  30370  poseq  30800  soseq  30801  funtransport  31114  funray  31223  funline  31225  fnessref  31328  neibastop2  31332  dissneqlem  32159  dissneq  32160  ptrest  32374  poimirlem27  32402  poimirlem32  32407  ismblfin  32416  volsupnfl  32420  itg2addnclem  32427  unirep  32473  filbcmb  32501  sdclem1  32505  sdc  32506  fdc  32507  incsequz  32510  heibor1lem  32574  heiborlem10  32585  isgrpda  32720  isdrngo2  32723  prnc  32832  prtlem13  32967  prtlem15  32974  lshpsmreu  33210  lshpkrlem1  33211  lshpkrlem3  33213  pclfinN  34000  4atex  34176  dihglblem2N  35397  lcfl7N  35604  lcf1o  35654  mzpcompact2lem  36128  eldioph3  36143  diophrex  36153  rexrabdioph  36172  eldioph4i  36190  aomclem8  36445  hbtlem2  36509  rngunsnply  36558  iunrelexpuztr  36826  ntrclsneine0lem  37178  dvconstbi  37351  expgrowth  37352  wessf1ornlem  38162  limcperiod  38492  limsupre  38505  cncfshiftioo  38575  itgiccshift  38669  itgperiod  38670  fourierdlem42  38839  fourierdlem48  38844  fourierdlem81  38877  fourierdlem92  38888  fourierdlem96  38892  fourierdlem97  38893  fourierdlem98  38894  fourierdlem99  38895  fourierdlem105  38901  fourierdlem108  38904  fourierdlem110  38906  fourierdlem112  38908  fourierdlem113  38909  hoidmvval0  39274  ovnhoi  39290  ovolval5lem3  39341  ovolval5  39342  fmtnofac2lem  39816  erclwwlkssym  41237  erclwwlkstr  41238  erclwwlksnsym  41249  erclwwlksntr  41250  eleclclwwlksn  41255  hashecclwwlksn1  41256  umgrhashecclwwlk  41257  frgrregorufr0  41484  2zlidl  41719  2zrngamgm  41724  2zrngagrp  41728  2zrngmmgm  41731
  Copyright terms: Public domain W3C validator