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

Theorem cbvrexv 2953
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 1673 . 2  |-  F/ y
ph
2 nfv 1673 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2949 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 2721
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725  df-rex 2726
This theorem is referenced by:  cbvrex2v  2961  reu7  3159  reusv3  4505  xpdifid  5271  fliftfun  6010  grpridd  6308  funcnvuni  6535  fun11iun  6542  nneob  7096  pssnn  7536  frfi  7562  finsschain  7623  marypha1lem  7688  supmo  7707  suplub2  7716  ordtypelem3  7739  ordtypelem9  7745  wemaplem1  7765  brwdom3  7802  unwdomg  7804  cantnf  7906  cantnfOLD  7928  trcl  7953  infxpenc2  8193  infxpenc2OLD  8197  aceq2  8294  dfac5lem4  8301  kmlem9  8332  kmlem14  8337  fin23lem26  8499  fin1a2lem13  8586  axdc3lem3  8626  winainflem  8865  axgroth4  9004  suprlub  10297  supmul1  10300  supmullem1  10301  supmullem2  10302  supmul  10303  ublbneg  10944  zsupss  10949  xrsupsslem  11274  xrinfmsslem  11275  rexanre  12839  rexuzre  12845  rexico  12846  caurcvg2  13160  caucvgb  13162  summolem2  13198  summo  13199  mertens  13351  odd2np1lem  13596  gcdcllem1  13700  pceu  13918  4sqlem12  14022  vdwlem10  14056  vdwlem13  14059  vdwnn  14064  drsdirfi  15113  gaorb  15830  psgnunilem3  16007  psgnunilem4  16008  psgneu  16017  pj1eu  16198  efgsfo  16241  cyggeninv  16365  cygabl  16372  pgpfac1lem5  16585  pgpfac1  16586  pgpfaclem2  16588  lss1d  17049  lspsneq  17208  lspsolvlem  17228  lbsextlem2  17245  mplcoe5lem  17552  cygznlem3  18007  ordtrest2lem  18812  cnprest  18898  1stcfb  19054  1stcelcls  19070  elpt  19150  fbssfi  19415  fgcl  19456  rnelfmlem  19530  fmfnfmlem3  19534  txflf  19584  alexsubb  19623  alexsubALTlem4  19627  isucn2  19859  icccmplem2  20405  ply1divex  21613  coeeu  21698  plydivex  21768  aannenlem2  21800  ulmcau  21865  ulmbdd  21868  dchrptlem2  22609  bposlem9  22636  pntibndlem3  22846  pntlemi  22858  pntlemp  22864  pntleml  22865  pnt3  22866  legval  23020  legov  23021  legov2  23022  isgrpo2  23689  grpoidinvlem3  23698  isgrp2d  23727  isgrpda  23789  ubthlem3  24278  norm1exi  24658  pjhthmo  24710  cdjreui  25841  cdj3i  25850  isarchi3  26209  archiabl  26220  ordtrest2NEWlem  26357  lmxrge0  26387  esumcvg  26540  eulerpartlems  26748  eulerpartlemgvv  26764  conpcon  27129  cvmlift2lem12  27208  cvmlift2lem13  27209  cvmlift3lem2  27214  cvmlift3lem7  27219  cvmlift3  27222  prodmolem2  27453  prodmo  27454  poseq  27719  soseq  27720  funtransport  28067  funray  28176  funline  28178  supaddc  28422  supadd  28423  ptrest  28430  ismblfin  28437  volsupnfl  28441  itg2addnclem  28448  fnessref  28570  neibastop2  28587  unirep  28611  filbcmb  28639  sdclem1  28644  sdc  28645  fdc  28646  incsequz  28649  heibor1lem  28713  heiborlem10  28724  isdrngo2  28769  prnc  28872  prtlem13  29018  prtlem15  29025  mzpcompact2lem  29093  eldioph3  29109  diophrex  29119  rexrabdioph  29137  eldioph4i  29156  aomclem8  29419  hbtlem2  29485  rngunsnply  29535  dvconstbi  29613  expgrowth  29614  erclwwlksym  30489  erclwwlktr  30490  erclwwlknsym  30505  erclwwlkntr  30506  eleclclwwlkn  30512  hashecclwwlkn1  30513  usghashecclwwlk  30514  frgraregorufr0  30650  fsuppmapnn0fiub  30804  scmatsubcl  30889  scmatmulcl  30891  lshpsmreu  32759  lshpkrlem1  32760  lshpkrlem3  32762  pclfinN  33549  4atex  33725  dihglblem2N  34944  lcfl7N  35151  lcf1o  35201
  Copyright terms: Public domain W3C validator