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

Theorem cbvrexv 2925
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 1629 . 2  |-  F/ y
ph
2 nfv 1629 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2921 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wrex 2698
This theorem is referenced by:  cbvrex2v  2933  reu7  3121  reusv3  4722  funcnvuni  5509  fun11iun  5686  fliftfun  6025  grpridd  6278  tfrlem3  6629  abianfp  6707  nneob  6886  pssnn  7318  frfi  7343  finsschain  7404  marypha1lem  7429  supmo  7446  suplub2  7455  ordtypelem3  7478  ordtypelem9  7484  wemaplem1  7504  brwdom3  7539  unwdomg  7541  cantnf  7638  trcl  7653  infxpenc2  7892  aceq2  7989  dfac5lem4  7996  kmlem9  8027  kmlem14  8032  fin23lem26  8194  fin1a2lem13  8281  axdc3lem3  8321  winainflem  8557  axgroth4  8696  suprlub  9959  supmul1  9962  supmullem1  9963  supmullem2  9964  supmul  9965  ublbneg  10549  zsupss  10554  xrsupsslem  10874  xrinfmsslem  10875  rexanre  12138  rexuzre  12144  rexico  12145  caurcvg2  12459  caucvgb  12461  summolem2  12498  summo  12499  mertens  12651  odd2np1lem  12895  gcdcllem1  12999  pceu  13208  4sqlem12  13312  vdwlem10  13346  vdwlem13  13349  vdwnn  13354  drsdirfi  14383  gaorb  15072  pj1eu  15316  efgsfo  15359  cyggeninv  15481  cygabl  15488  pgpfac1lem5  15625  pgpfac1  15626  pgpfaclem2  15628  lss1d  16027  lspsneq  16182  lspsolvlem  16202  lbsextlem2  16219  cygznlem3  16838  ordtrest2lem  17255  cnprest  17341  1stcfb  17496  1stcelcls  17512  elpt  17592  fbssfi  17857  fgcl  17898  rnelfmlem  17972  fmfnfmlem3  17976  txflf  18026  alexsubb  18065  alexsubALTlem4  18069  isucn2  18297  icccmplem2  18842  ply1divex  20047  coeeu  20132  plydivex  20202  aannenlem2  20234  ulmcau  20299  ulmbdd  20302  dchrptlem2  21037  bposlem9  21064  pntibndlem3  21274  pntlemi  21286  pntlemp  21292  pntleml  21293  pnt3  21294  isgrpo2  21773  grpoidinvlem3  21782  isgrp2d  21811  isgrpda  21873  ubthlem3  22362  norm1exi  22740  pjhthmo  22792  cdjreui  23923  cdj3i  23932  lmxrge0  24325  esumcvg  24464  conpcon  24910  cvmlift2lem12  24989  cvmlift2lem13  24990  cvmlift3lem2  24995  cvmlift3lem7  25000  cvmlift3  25003  prodmolem2  25250  prodmo  25251  poseq  25508  soseq  25509  funtransport  25913  funray  26022  funline  26024  supaddc  26184  supadd  26185  ismblfin  26193  volsupnfl  26197  itg2addnclem  26202  fnessref  26310  neibastop2  26327  unirep  26351  filbcmb  26379  sdclem1  26384  sdc  26385  fdc  26386  incsequz  26389  heibor1lem  26455  heiborlem10  26466  isdrngo2  26511  prnc  26614  prtlem13  26654  prtlem15  26661  mzpcompact2lem  26745  eldioph3  26761  diophrex  26771  rexrabdioph  26791  eldioph4i  26810  aomclem8  27074  hbtlem2  27243  rngunsnply  27293  psgnunilem3  27334  psgnunilem4  27335  psgneu  27344  dvconstbi  27466  expgrowth  27467  frgraregorufr0  28299  lshpsmreu  29746  lshpkrlem1  29747  lshpkrlem3  29749  pclfinN  30536  4atex  30712  dihglblem2N  31931  lcfl7N  32138  lcf1o  32188
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703
  Copyright terms: Public domain W3C validator