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

Theorem cbvrexv 2841
Description: Change the bound variable of a restricted existential quantifier using implicit substitution. (Contributed by NM, 2-Jun-1998.)
Hypothesis
Ref Expression
cbvralv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrexv  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Distinct variable groups:    x, A    y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrexv
StepHypRef Expression
1 nfv 1619 . 2  |-  F/ y
ph
2 nfv 1619 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2837 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wrex 2620
This theorem is referenced by:  cbvrex2v  2849  reu7  3036  reusv3  4624  funcnvuni  5399  fun11iun  5576  fliftfun  5898  grpridd  6147  tfrlem3  6480  abianfp  6558  nneob  6737  pssnn  7169  frfi  7192  finsschain  7252  marypha1lem  7276  supmo  7293  suplub2  7302  ordtypelem3  7325  ordtypelem9  7331  wemaplem1  7351  brwdom3  7386  unwdomg  7388  cantnf  7485  trcl  7500  infxpenc2  7739  aceq2  7836  dfac5lem4  7843  kmlem9  7874  kmlem14  7879  fin23lem26  8041  fin1a2lem13  8128  axdc3lem3  8168  winainflem  8405  axgroth4  8544  suprlub  9806  supmul1  9809  supmullem1  9810  supmullem2  9811  supmul  9812  ublbneg  10394  zsupss  10399  xrsupsslem  10717  xrinfmsslem  10718  rexanre  11926  rexuzre  11932  rexico  11933  caurcvg2  12247  caucvgb  12249  summolem2  12286  summo  12287  mertens  12439  odd2np1lem  12683  gcdcllem1  12787  pceu  12996  4sqlem12  13100  vdwlem10  13134  vdwlem13  13137  vdwnn  13142  drsdirfi  14171  gaorb  14860  pj1eu  15104  efgsfo  15147  cyggeninv  15269  cygabl  15276  pgpfac1lem5  15413  pgpfac1  15414  pgpfaclem2  15416  lss1d  15819  lspsneq  15974  lspsolvlem  15994  lbsextlem2  16011  cygznlem3  16629  ordtrest2lem  17039  cnprest  17123  1stcfb  17277  1stcelcls  17293  elpt  17373  fbssfi  17634  fgcl  17675  rnelfmlem  17749  fmfnfmlem3  17753  txflf  17803  alexsubb  17842  alexsubALTlem4  17846  icccmplem2  18431  ply1divex  19626  coeeu  19711  plydivex  19781  aannenlem2  19813  ulmcau  19878  ulmbdd  19881  dchrptlem2  20616  bposlem9  20643  pntibndlem3  20853  pntlemi  20865  pntlemp  20871  pntleml  20872  pnt3  20873  isgrpo2  20976  grpoidinvlem3  20985  isgrp2d  21014  isgrpda  21076  ubthlem3  21565  norm1exi  21943  pjhthmo  21995  cdjreui  23126  cdj3i  23135  lmxrge0  23493  esumcvg  23742  conpcon  24170  cvmlift2lem12  24249  cvmlift2lem13  24250  cvmlift3lem2  24255  cvmlift3lem7  24260  cvmlift3  24263  prodmolem2  24562  prodmo  24563  poseq  24811  soseq  24812  funtransport  25213  funray  25322  funline  25324  supaddc  25482  supadd  25483  volsupnfl  25491  itg2addnclem  25492  itg2addnc  25494  fnessref  25617  neibastop2  25634  unirep  25673  filbcmb  25756  sdclem1  25777  sdc  25778  fdc  25779  incsequz  25782  heibor1lem  25856  heiborlem10  25867  isdrngo2  25912  prnc  26015  prtlem13  26059  prtlem15  26066  mzpcompact2lem  26152  eldioph3  26168  diophrex  26178  rexrabdioph  26198  eldioph4i  26218  aomclem8  26482  hbtlem2  26651  rngunsnply  26701  psgnunilem3  26742  psgnunilem4  26743  psgneu  26752  dvconstbi  26874  expgrowth  26875  frgraregorufr0  27885  lshpsmreu  29368  lshpkrlem1  29369  lshpkrlem3  29371  pclfinN  30158  4atex  30334  dihglblem2N  31553  lcfl7N  31760  lcf1o  31810
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-rex 2625
  Copyright terms: Public domain W3C validator