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

Theorem cbvrexv 2939
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 1630 . 2  |-  F/ y
ph
2 nfv 1630 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2935 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   E.wrex 2712
This theorem is referenced by:  cbvrex2v  2947  reu7  3135  reusv3  4760  funcnvuni  5547  fun11iun  5724  fliftfun  6063  grpridd  6316  tfrlem3  6667  abianfp  6745  nneob  6924  pssnn  7356  frfi  7381  finsschain  7442  marypha1lem  7467  supmo  7486  suplub2  7495  ordtypelem3  7518  ordtypelem9  7524  wemaplem1  7544  brwdom3  7579  unwdomg  7581  cantnf  7678  trcl  7693  infxpenc2  7934  aceq2  8031  dfac5lem4  8038  kmlem9  8069  kmlem14  8074  fin23lem26  8236  fin1a2lem13  8323  axdc3lem3  8363  winainflem  8599  axgroth4  8738  suprlub  10001  supmul1  10004  supmullem1  10005  supmullem2  10006  supmul  10007  ublbneg  10591  zsupss  10596  xrsupsslem  10916  xrinfmsslem  10917  rexanre  12181  rexuzre  12187  rexico  12188  caurcvg2  12502  caucvgb  12504  summolem2  12541  summo  12542  mertens  12694  odd2np1lem  12938  gcdcllem1  13042  pceu  13251  4sqlem12  13355  vdwlem10  13389  vdwlem13  13392  vdwnn  13397  drsdirfi  14426  gaorb  15115  pj1eu  15359  efgsfo  15402  cyggeninv  15524  cygabl  15531  pgpfac1lem5  15668  pgpfac1  15669  pgpfaclem2  15671  lss1d  16070  lspsneq  16225  lspsolvlem  16245  lbsextlem2  16262  cygznlem3  16881  ordtrest2lem  17298  cnprest  17384  1stcfb  17539  1stcelcls  17555  elpt  17635  fbssfi  17900  fgcl  17941  rnelfmlem  18015  fmfnfmlem3  18019  txflf  18069  alexsubb  18108  alexsubALTlem4  18112  isucn2  18340  icccmplem2  18885  ply1divex  20090  coeeu  20175  plydivex  20245  aannenlem2  20277  ulmcau  20342  ulmbdd  20345  dchrptlem2  21080  bposlem9  21107  pntibndlem3  21317  pntlemi  21329  pntlemp  21335  pntleml  21336  pnt3  21337  isgrpo2  21816  grpoidinvlem3  21825  isgrp2d  21854  isgrpda  21916  ubthlem3  22405  norm1exi  22783  pjhthmo  22835  cdjreui  23966  cdj3i  23975  lmxrge0  24368  esumcvg  24507  conpcon  24953  cvmlift2lem12  25032  cvmlift2lem13  25033  cvmlift3lem2  25038  cvmlift3lem7  25043  cvmlift3  25046  prodmolem2  25292  prodmo  25293  poseq  25559  soseq  25560  funtransport  25996  funray  26105  funline  26107  supaddc  26269  supadd  26270  ismblfin  26283  volsupnfl  26287  itg2addnclem  26294  fnessref  26411  neibastop2  26428  unirep  26452  filbcmb  26480  sdclem1  26485  sdc  26486  fdc  26487  incsequz  26490  heibor1lem  26556  heiborlem10  26567  isdrngo2  26612  prnc  26715  prtlem13  26755  prtlem15  26762  mzpcompact2lem  26846  eldioph3  26862  diophrex  26872  rexrabdioph  26892  eldioph4i  26911  aomclem8  27174  hbtlem2  27343  rngunsnply  27393  psgnunilem3  27434  psgnunilem4  27435  psgneu  27444  dvconstbi  27566  expgrowth  27567  frgraregorufr0  28539  lshpsmreu  30005  lshpkrlem1  30006  lshpkrlem3  30008  pclfinN  30795  4atex  30971  dihglblem2N  32190  lcfl7N  32397  lcf1o  32447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ral 2716  df-rex 2717
  Copyright terms: Public domain W3C validator