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

Theorem cbvrexv 3082
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 1712 . 2  |-  F/ y
ph
2 nfv 1712 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 3078 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1618  df-nf 1622  df-sb 1745  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809  df-rex 2810
This theorem is referenced by:  cbvrex2v  3090  reu7  3291  reusv3  4645  xpdifid  5420  fliftfun  6185  grpridd  6488  funcnvuni  6726  fun11iun  6733  nneob  7293  pssnn  7731  frfi  7757  finsschain  7819  marypha1lem  7885  supmo  7903  suplub2  7912  ordtypelem3  7937  ordtypelem9  7943  wemaplem1  7963  brwdom3  8000  unwdomg  8002  cantnf  8103  cantnfOLD  8125  trcl  8150  infxpenc2  8390  infxpenc2OLD  8394  aceq2  8491  dfac5lem4  8498  kmlem9  8529  kmlem14  8534  fin23lem26  8696  fin1a2lem13  8783  axdc3lem3  8823  winainflem  9060  axgroth4  9199  suprlub  10500  supmul1  10503  supmullem1  10504  supmullem2  10505  supmul  10506  ublbneg  11167  zsupss  11172  xrsupsslem  11501  xrinfmsslem  11502  fsuppmapnn0fiub  12079  rexanre  13261  rexuzre  13267  rexico  13268  caurcvg2  13582  caucvgb  13584  summolem2  13620  summo  13621  mertens  13777  prodmolem2  13824  prodmo  13825  odd2np1lem  14129  gcdcllem1  14233  pceu  14454  4sqlem12  14558  vdwlem10  14592  vdwlem13  14595  vdwnn  14600  drsdirfi  15766  gaorb  16544  psgnunilem3  16720  psgnunilem4  16721  psgneu  16730  pj1eu  16913  efgsfo  16956  cyggeninv  17085  cygabl  17092  pgpfac1lem5  17325  pgpfac1  17326  pgpfaclem2  17328  lss1d  17804  lspsneq  17963  lspsolvlem  17983  lbsextlem2  18000  mplcoe5lem  18325  cygznlem3  18781  pmatcollpw3fi1lem2  19455  ordtrest2lem  19871  cnprest  19957  1stcfb  20112  1stcelcls  20128  elpt  20239  fbssfi  20504  fgcl  20545  rnelfmlem  20619  fmfnfmlem3  20623  txflf  20673  alexsubb  20712  alexsubALTlem4  20716  isucn2  20948  icccmplem2  21494  ply1divex  22703  coeeu  22788  plydivex  22859  aannenlem2  22891  ulmcau  22956  ulmbdd  22959  dchrptlem2  23738  bposlem9  23765  pntibndlem3  23975  pntlemi  23987  pntlemp  23993  pntleml  23994  pnt3  23995  legval  24172  legov  24173  legov2  24174  lnopp2hpgb  24333  erclwwlksym  25016  erclwwlktr  25017  erclwwlknsym  25028  erclwwlkntr  25029  eleclclwwlkn  25035  hashecclwwlkn1  25036  usghashecclwwlk  25037  frgraregorufr0  25254  isgrpo2  25397  grpoidinvlem3  25406  isgrp2d  25435  isgrpda  25497  ubthlem3  25986  norm1exi  26366  pjhthmo  26418  cdjreui  27549  cdj3i  27558  isarchi3  27965  archiabl  27976  ordtrest2NEWlem  28139  lmxrge0  28169  esumcvg  28315  esum2d  28322  eulerpartlems  28563  eulerpartlemgvv  28579  conpcon  28944  cvmlift2lem12  29023  cvmlift2lem13  29024  cvmlift3lem2  29029  cvmlift3lem7  29034  cvmlift3  29037  poseq  29573  soseq  29574  funtransport  29909  funray  30018  funline  30020  supaddc  30281  supadd  30282  ptrest  30288  ismblfin  30295  volsupnfl  30299  itg2addnclem  30306  fnessref  30415  neibastop2  30419  unirep  30443  filbcmb  30471  sdclem1  30476  sdc  30477  fdc  30478  incsequz  30481  heibor1lem  30545  heiborlem10  30556  isdrngo2  30601  prnc  30704  prtlem13  30849  prtlem15  30856  mzpcompact2lem  30923  eldioph3  30938  diophrex  30948  rexrabdioph  30967  eldioph4i  30985  aomclem8  31246  hbtlem2  31314  rngunsnply  31363  dvconstbi  31480  expgrowth  31481  limcperiod  31873  limsupre  31886  cncfshiftioo  31934  itgiccshift  32018  itgperiod  32019  fourierdlem42  32170  fourierdlem48  32176  fourierdlem81  32209  fourierdlem92  32220  fourierdlem96  32224  fourierdlem97  32225  fourierdlem98  32226  fourierdlem99  32227  fourierdlem105  32233  fourierdlem108  32236  fourierdlem110  32238  fourierdlem112  32240  fourierdlem113  32241  2zlidl  32994  2zrngamgm  32999  2zrngagrp  33003  2zrngmmgm  33006  lshpsmreu  35231  lshpkrlem1  35232  lshpkrlem3  35234  pclfinN  36021  4atex  36197  dihglblem2N  37418  lcfl7N  37625  lcf1o  37675  iunrelexpuztr  38206
  Copyright terms: Public domain W3C validator