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

Theorem cbvrexv 3054
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 1751 . 2  |-  F/ y
ph
2 nfv 1751 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 3050 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187   E.wrex 2774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-ex 1660  df-nf 1664  df-sb 1787  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ral 2778  df-rex 2779
This theorem is referenced by:  cbvrex2v  3062  reu7  3263  reusv3  4624  xpdifid  5276  fliftfun  6211  grpridd  6514  funcnvuni  6751  fun11iun  6758  nneob  7352  pssnn  7787  frfi  7813  finsschain  7878  marypha1lem  7944  supmo  7963  suplub2  7972  ordtypelem3  8026  ordtypelem9  8032  wemaplem1  8052  brwdom3  8088  unwdomg  8090  cantnf  8188  trcl  8202  infxpenc2  8442  aceq2  8539  dfac5lem4  8546  kmlem9  8577  kmlem14  8582  fin23lem26  8744  fin1a2lem13  8831  axdc3lem3  8871  winainflem  9107  axgroth4  9246  suprlub  10560  supaddc  10563  supadd  10564  supmul1  10565  supmullem1  10566  supmullem2  10567  supmul  10568  ublbneg  11237  zsupss  11242  xrsupsslem  11581  xrinfmsslem  11582  fsuppmapnn0fiub  12189  rexanre  13377  rexuzre  13383  rexico  13384  caurcvg2  13711  caucvgb  13713  summolem2  13749  summo  13750  mertens  13909  prodmolem2  13956  prodmo  13957  odd2np1lem  14331  gcdcllem1  14436  pceu  14748  4sqlem12  14852  vdwlem10  14892  vdwlem13  14895  vdwnn  14900  drsdirfi  16127  gaorb  16905  psgnunilem3  17081  psgnunilem4  17082  psgneu  17091  pj1eu  17274  efgsfo  17317  cyggeninv  17446  cygabl  17453  pgpfac1lem5  17640  pgpfac1  17641  pgpfaclem2  17643  lss1d  18114  lspsneq  18273  lspsolvlem  18293  lbsextlem2  18310  mplcoe5lem  18619  cygznlem3  19064  pmatcollpw3fi1lem2  19735  ordtrest2lem  20143  cnprest  20229  1stcfb  20384  1stcelcls  20400  elpt  20511  fbssfi  20776  fgcl  20817  rnelfmlem  20891  fmfnfmlem3  20895  txflf  20945  alexsubb  20985  alexsubALTlem4  20989  isucn2  21218  icccmplem2  21745  ply1divex  22959  coeeu  23044  plydivex  23115  aannenlem2  23147  ulmcau  23212  ulmbdd  23215  dchrptlem2  24053  bposlem9  24080  pntibndlem3  24290  pntlemi  24302  pntlemp  24308  pntleml  24309  pnt3  24310  legval  24486  legov  24487  legov2  24488  outpasch  24651  lnopp2hpgb  24658  colopp  24664  erclwwlksym  25384  erclwwlktr  25385  erclwwlknsym  25396  erclwwlkntr  25397  eleclclwwlkn  25403  hashecclwwlkn1  25404  usghashecclwwlk  25405  frgraregorufr0  25622  isgrpo2  25767  grpoidinvlem3  25776  isgrp2d  25805  isgrpda  25867  ubthlem3  26356  norm1exi  26735  pjhthmo  26787  cdjreui  27917  cdj3i  27926  infxrge0glb  28183  isarchi3  28339  archiabl  28350  ordtrest2NEWlem  28564  lmxrge0  28594  esumcvg  28743  esum2d  28750  eulerpartlems  29016  eulerpartlemgvv  29032  conpcon  29743  cvmlift2lem12  29822  cvmlift2lem13  29823  cvmlift3lem2  29828  cvmlift3lem7  29833  cvmlift3  29836  poseq  30275  soseq  30276  funtransport  30580  funray  30689  funline  30691  fnessref  30795  neibastop2  30799  dissneqlem  31473  dissneq  31474  ptrest  31643  poimirlem27  31671  poimirlem32  31676  ismblfin  31685  volsupnfl  31689  itg2addnclem  31697  unirep  31743  filbcmb  31771  sdclem1  31776  sdc  31777  fdc  31778  incsequz  31781  heibor1lem  31845  heiborlem10  31856  isdrngo2  31901  prnc  32004  prtlem13  32148  prtlem15  32155  lshpsmreu  32384  lshpkrlem1  32385  lshpkrlem3  32387  pclfinN  33174  4atex  33350  dihglblem2N  34571  lcfl7N  34778  lcf1o  34828  mzpcompact2lem  35302  eldioph3  35317  diophrex  35327  rexrabdioph  35346  eldioph4i  35364  aomclem8  35629  hbtlem2  35693  rngunsnply  35742  iunrelexpuztr  35954  dvconstbi  36324  expgrowth  36325  wessf1ornlem  37086  limcperiod  37284  limsupre  37297  limsupreOLD  37298  cncfshiftioo  37346  itgiccshift  37430  itgperiod  37431  fourierdlem42  37584  fourierdlem48  37590  fourierdlem81  37623  fourierdlem92  37634  fourierdlem96  37638  fourierdlem97  37639  fourierdlem98  37640  fourierdlem99  37641  fourierdlem105  37647  fourierdlem108  37650  fourierdlem110  37652  fourierdlem112  37654  fourierdlem113  37655  2zlidl  38705  2zrngamgm  38710  2zrngagrp  38714  2zrngmmgm  38717
  Copyright terms: Public domain W3C validator