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

Theorem cbvrexv 3020
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 1761 . 2  |-  F/ y
ph
2 nfv 1761 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 3016 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   E.wrex 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1664  df-nf 1668  df-sb 1798  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-rex 2743
This theorem is referenced by:  cbvrex2v  3028  reu7  3233  reusv3  4611  xpdifid  5265  fliftfun  6205  grpridd  6509  funcnvuni  6746  fun11iun  6753  nneob  7353  pssnn  7790  frfi  7816  finsschain  7881  marypha1lem  7947  supmo  7966  suplub2  7975  infmo  8011  ordtypelem3  8035  ordtypelem9  8041  wemaplem1  8061  brwdom3  8097  unwdomg  8099  cantnf  8198  trcl  8212  infxpenc2  8453  aceq2  8550  dfac5lem4  8557  kmlem9  8588  kmlem14  8593  fin23lem26  8755  fin1a2lem13  8842  axdc3lem3  8882  winainflem  9118  axgroth4  9257  suprlub  10571  supaddc  10574  supadd  10575  supmul1  10576  supmullem1  10577  supmullem2  10578  supmul  10579  ublbneg  11248  zsupss  11253  xrsupsslem  11592  xrinfmsslem  11593  fsuppmapnn0fiub  12203  rexanre  13409  rexuzre  13415  rexico  13416  caurcvg2  13744  caucvgb  13746  summolem2  13782  summo  13783  mertens  13942  prodmolem2  13989  prodmo  13990  odd2np1lem  14364  gcdcllem1  14473  pceu  14796  4sqlem12  14900  vdwlem10  14940  vdwlem13  14943  vdwnn  14948  drsdirfi  16183  gaorb  16961  psgnunilem3  17137  psgnunilem4  17138  psgneu  17147  pj1eu  17346  efgsfo  17389  cyggeninv  17518  cygabl  17525  pgpfac1lem5  17712  pgpfac1  17713  pgpfaclem2  17715  lss1d  18186  lspsneq  18345  lspsolvlem  18365  lbsextlem2  18382  mplcoe5lem  18691  cygznlem3  19140  pmatcollpw3fi1lem2  19811  ordtrest2lem  20219  cnprest  20305  1stcfb  20460  1stcelcls  20476  elpt  20587  fbssfi  20852  fgcl  20893  rnelfmlem  20967  fmfnfmlem3  20971  txflf  21021  alexsubb  21061  alexsubALTlem4  21065  isucn2  21294  icccmplem2  21841  ply1divex  23087  coeeu  23179  plydivex  23250  aannenlem2  23285  ulmcau  23350  ulmbdd  23353  dchrptlem2  24193  bposlem9  24220  pntibndlem3  24430  pntlemi  24442  pntlemp  24448  pntleml  24449  pnt3  24450  legval  24629  legov  24630  legov2  24631  outpasch  24797  lnopp2hpgb  24805  colopp  24811  erclwwlksym  25542  erclwwlktr  25543  erclwwlknsym  25554  erclwwlkntr  25555  eleclclwwlkn  25561  hashecclwwlkn1  25562  usghashecclwwlk  25563  frgraregorufr0  25780  isgrpo2  25925  grpoidinvlem3  25934  isgrp2d  25963  isgrpda  26025  ubthlem3  26514  norm1exi  26903  pjhthmo  26955  cdjreui  28085  cdj3i  28094  infxrge0glb  28348  infxrge0glbOLD  28349  isarchi3  28504  archiabl  28515  ordtrest2NEWlem  28728  lmxrge0  28758  esumcvg  28907  esum2d  28914  eulerpartlems  29193  eulerpartlemgvv  29209  conpcon  29958  cvmlift2lem12  30037  cvmlift2lem13  30038  cvmlift3lem2  30043  cvmlift3lem7  30048  cvmlift3  30051  poseq  30491  soseq  30492  funtransport  30798  funray  30907  funline  30909  fnessref  31013  neibastop2  31017  dissneqlem  31742  dissneq  31743  ptrest  31939  poimirlem27  31967  poimirlem32  31972  ismblfin  31981  volsupnfl  31985  itg2addnclem  31993  unirep  32039  filbcmb  32067  sdclem1  32072  sdc  32073  fdc  32074  incsequz  32077  heibor1lem  32141  heiborlem10  32152  isdrngo2  32197  prnc  32300  prtlem13  32440  prtlem15  32447  lshpsmreu  32675  lshpkrlem1  32676  lshpkrlem3  32678  pclfinN  33465  4atex  33641  dihglblem2N  34862  lcfl7N  35069  lcf1o  35119  mzpcompact2lem  35593  eldioph3  35608  diophrex  35618  rexrabdioph  35637  eldioph4i  35655  aomclem8  35919  hbtlem2  35983  rngunsnply  36039  iunrelexpuztr  36311  dvconstbi  36683  expgrowth  36684  wessf1ornlem  37459  limcperiod  37708  limsupre  37721  limsupreOLD  37722  cncfshiftioo  37770  itgiccshift  37857  itgperiod  37858  fourierdlem42  38012  fourierdlem42OLD  38013  fourierdlem48  38018  fourierdlem81  38051  fourierdlem92  38062  fourierdlem96  38066  fourierdlem97  38067  fourierdlem98  38068  fourierdlem99  38069  fourierdlem105  38075  fourierdlem108  38078  fourierdlem110  38080  fourierdlem112  38082  fourierdlem113  38083  hoidmvval0  38409  ovnhoi  38425  2zlidl  39987  2zrngamgm  39992  2zrngagrp  39996  2zrngmmgm  39999
  Copyright terms: Public domain W3C validator