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  4621  funcnvuni  5396  fun11iun  5573  fliftfun  5895  grpridd  6144  tfrlem3  6477  abianfp  6555  nneob  6734  pssnn  7166  frfi  7189  finsschain  7249  marypha1lem  7273  supmo  7290  suplub2  7299  ordtypelem3  7322  ordtypelem9  7328  wemaplem1  7348  brwdom3  7383  unwdomg  7385  cantnf  7482  trcl  7497  infxpenc2  7736  aceq2  7833  dfac5lem4  7840  kmlem9  7871  kmlem14  7876  fin23lem26  8038  fin1a2lem13  8125  axdc3lem3  8165  winainflem  8402  axgroth4  8541  suprlub  9803  supmul1  9806  supmullem1  9807  supmullem2  9808  supmul  9809  ublbneg  10391  zsupss  10396  xrsupsslem  10714  xrinfmsslem  10715  rexanre  11920  rexuzre  11926  rexico  11927  caurcvg2  12241  caucvgb  12243  summolem2  12280  summo  12281  mertens  12433  odd2np1lem  12677  gcdcllem1  12781  pceu  12990  4sqlem12  13094  vdwlem10  13128  vdwlem13  13131  vdwnn  13136  drsdirfi  14165  gaorb  14854  pj1eu  15098  efgsfo  15141  cyggeninv  15263  cygabl  15270  pgpfac1lem5  15407  pgpfac1  15408  pgpfaclem2  15410  lss1d  15813  lspsneq  15968  lspsolvlem  15988  lbsextlem2  16005  cygznlem3  16623  ordtrest2lem  17033  cnprest  17117  1stcfb  17271  1stcelcls  17287  elpt  17367  fbssfi  17628  fgcl  17669  rnelfmlem  17743  fmfnfmlem3  17747  txflf  17797  alexsubb  17836  alexsubALTlem4  17840  icccmplem2  18425  ply1divex  19620  coeeu  19705  plydivex  19775  aannenlem2  19807  ulmcau  19872  ulmbdd  19875  dchrptlem2  20610  bposlem9  20637  pntibndlem3  20847  pntlemi  20859  pntlemp  20865  pntleml  20866  pnt3  20867  isgrpo2  20970  grpoidinvlem3  20979  isgrp2d  21008  isgrpda  21070  ubthlem3  21559  norm1exi  21937  pjhthmo  21989  cdjreui  23120  cdj3i  23129  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  27868  lshpsmreu  29351  lshpkrlem1  29352  lshpkrlem3  29354  pclfinN  30141  4atex  30317  dihglblem2N  31536  lcfl7N  31743  lcf1o  31793
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