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

Theorem cbvrexv 2901
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 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 2897 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wrex 2675
This theorem is referenced by:  cbvrex2v  2909  reu7  3097  reusv3  4698  funcnvuni  5485  fun11iun  5662  fliftfun  6001  grpridd  6254  tfrlem3  6605  abianfp  6683  nneob  6862  pssnn  7294  frfi  7319  finsschain  7379  marypha1lem  7404  supmo  7421  suplub2  7430  ordtypelem3  7453  ordtypelem9  7459  wemaplem1  7479  brwdom3  7514  unwdomg  7516  cantnf  7613  trcl  7628  infxpenc2  7867  aceq2  7964  dfac5lem4  7971  kmlem9  8002  kmlem14  8007  fin23lem26  8169  fin1a2lem13  8256  axdc3lem3  8296  winainflem  8532  axgroth4  8671  suprlub  9934  supmul1  9937  supmullem1  9938  supmullem2  9939  supmul  9940  ublbneg  10524  zsupss  10529  xrsupsslem  10849  xrinfmsslem  10850  rexanre  12113  rexuzre  12119  rexico  12120  caurcvg2  12434  caucvgb  12436  summolem2  12473  summo  12474  mertens  12626  odd2np1lem  12870  gcdcllem1  12974  pceu  13183  4sqlem12  13287  vdwlem10  13321  vdwlem13  13324  vdwnn  13329  drsdirfi  14358  gaorb  15047  pj1eu  15291  efgsfo  15334  cyggeninv  15456  cygabl  15463  pgpfac1lem5  15600  pgpfac1  15601  pgpfaclem2  15603  lss1d  16002  lspsneq  16157  lspsolvlem  16177  lbsextlem2  16194  cygznlem3  16813  ordtrest2lem  17229  cnprest  17315  1stcfb  17469  1stcelcls  17485  elpt  17565  fbssfi  17830  fgcl  17871  rnelfmlem  17945  fmfnfmlem3  17949  txflf  17999  alexsubb  18038  alexsubALTlem4  18042  isucn2  18270  icccmplem2  18815  ply1divex  20020  coeeu  20105  plydivex  20175  aannenlem2  20207  ulmcau  20272  ulmbdd  20275  dchrptlem2  21010  bposlem9  21037  pntibndlem3  21247  pntlemi  21259  pntlemp  21265  pntleml  21266  pnt3  21267  isgrpo2  21746  grpoidinvlem3  21755  isgrp2d  21784  isgrpda  21846  ubthlem3  22335  norm1exi  22713  pjhthmo  22765  cdjreui  23896  cdj3i  23905  lmxrge0  24298  esumcvg  24437  conpcon  24883  cvmlift2lem12  24962  cvmlift2lem13  24963  cvmlift3lem2  24968  cvmlift3lem7  24973  cvmlift3  24976  prodmolem2  25222  prodmo  25223  poseq  25475  soseq  25476  funtransport  25877  funray  25986  funline  25988  supaddc  26145  supadd  26146  ismblfin  26154  volsupnfl  26158  itg2addnclem  26163  fnessref  26271  neibastop2  26288  unirep  26312  filbcmb  26340  sdclem1  26345  sdc  26346  fdc  26347  incsequz  26350  heibor1lem  26416  heiborlem10  26427  isdrngo2  26472  prnc  26575  prtlem13  26615  prtlem15  26622  mzpcompact2lem  26706  eldioph3  26722  diophrex  26732  rexrabdioph  26752  eldioph4i  26771  aomclem8  27035  hbtlem2  27204  rngunsnply  27254  psgnunilem3  27295  psgnunilem4  27296  psgneu  27305  dvconstbi  27427  expgrowth  27428  frgraregorufr0  28163  lshpsmreu  29604  lshpkrlem1  29605  lshpkrlem3  29607  pclfinN  30394  4atex  30570  dihglblem2N  31789  lcfl7N  31996  lcf1o  32046
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rex 2680
  Copyright terms: Public domain W3C validator