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

Theorem cbvrexv 2938
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 1672 . 2  |-  F/ y
ph
2 nfv 1672 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2934 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 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711
This theorem is referenced by:  cbvrex2v  2946  reu7  3143  reusv3  4488  xpdifid  5254  fliftfun  5992  grpridd  6292  funcnvuni  6519  fun11iun  6526  abianfp  6900  nneob  7079  pssnn  7519  frfi  7545  finsschain  7606  marypha1lem  7671  supmo  7690  suplub2  7699  ordtypelem3  7722  ordtypelem9  7728  wemaplem1  7748  brwdom3  7785  unwdomg  7787  cantnf  7889  cantnfOLD  7911  trcl  7936  infxpenc2  8176  infxpenc2OLD  8180  aceq2  8277  dfac5lem4  8284  kmlem9  8315  kmlem14  8320  fin23lem26  8482  fin1a2lem13  8569  axdc3lem3  8609  winainflem  8847  axgroth4  8986  suprlub  10279  supmul1  10282  supmullem1  10283  supmullem2  10284  supmul  10285  ublbneg  10926  zsupss  10931  xrsupsslem  11256  xrinfmsslem  11257  rexanre  12817  rexuzre  12823  rexico  12824  caurcvg2  13138  caucvgb  13140  summolem2  13176  summo  13177  mertens  13328  odd2np1lem  13573  gcdcllem1  13677  pceu  13895  4sqlem12  13999  vdwlem10  14033  vdwlem13  14036  vdwnn  14041  drsdirfi  15090  gaorb  15804  psgnunilem3  15981  psgnunilem4  15982  psgneu  15991  pj1eu  16172  efgsfo  16215  cyggeninv  16339  cygabl  16346  pgpfac1lem5  16553  pgpfac1  16554  pgpfaclem2  16556  lss1d  16965  lspsneq  17124  lspsolvlem  17144  lbsextlem2  17161  cygznlem3  17843  ordtrest2lem  18648  cnprest  18734  1stcfb  18890  1stcelcls  18906  elpt  18986  fbssfi  19251  fgcl  19292  rnelfmlem  19366  fmfnfmlem3  19370  txflf  19420  alexsubb  19459  alexsubALTlem4  19463  isucn2  19695  icccmplem2  20241  ply1divex  21492  coeeu  21577  plydivex  21647  aannenlem2  21679  ulmcau  21744  ulmbdd  21747  dchrptlem2  22488  bposlem9  22515  pntibndlem3  22725  pntlemi  22737  pntlemp  22743  pntleml  22744  pnt3  22745  legval  22890  legov  22891  legov2  22892  isgrpo2  23506  grpoidinvlem3  23515  isgrp2d  23544  isgrpda  23606  ubthlem3  24095  norm1exi  24475  pjhthmo  24527  cdjreui  25658  cdj3i  25667  isarchi3  26027  archiabl  26038  ordtrest2NEWlem  26205  lmxrge0  26235  esumcvg  26388  eulerpartlems  26590  eulerpartlemgvv  26606  conpcon  26971  cvmlift2lem12  27050  cvmlift2lem13  27051  cvmlift3lem2  27056  cvmlift3lem7  27061  cvmlift3  27064  prodmolem2  27294  prodmo  27295  poseq  27560  soseq  27561  funtransport  27908  funray  28017  funline  28019  supaddc  28258  supadd  28259  ptrest  28266  ismblfin  28273  volsupnfl  28277  itg2addnclem  28284  fnessref  28406  neibastop2  28423  unirep  28447  filbcmb  28475  sdclem1  28480  sdc  28481  fdc  28482  incsequz  28485  heibor1lem  28549  heiborlem10  28560  isdrngo2  28605  prnc  28708  prtlem13  28855  prtlem15  28862  mzpcompact2lem  28930  eldioph3  28946  diophrex  28956  rexrabdioph  28974  eldioph4i  28993  aomclem8  29256  hbtlem2  29322  rngunsnply  29372  dvconstbi  29450  expgrowth  29451  erclwwlksym  30327  erclwwlktr  30328  erclwwlknsym  30343  erclwwlkntr  30344  eleclclwwlkn  30350  hashecclwwlkn1  30351  usghashecclwwlk  30352  frgraregorufr0  30488  lshpsmreu  32324  lshpkrlem1  32325  lshpkrlem3  32327  pclfinN  33114  4atex  33290  dihglblem2N  34509  lcfl7N  34716  lcf1o  34766
  Copyright terms: Public domain W3C validator