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

Theorem cbvrexv 3006
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 1769 . 2  |-  F/ y
ph
2 nfv 1769 . 2  |-  F/ x ps
3 cbvralv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvrex 3002 1  |-  ( E. x  e.  A  ph  <->  E. y  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   E.wrex 2757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-rex 2762
This theorem is referenced by:  cbvrex2v  3014  reu7  3221  reusv3  4609  xpdifid  5271  fliftfun  6223  grpridd  6528  funcnvuni  6765  fun11iun  6772  nneob  7371  pssnn  7808  frfi  7834  finsschain  7899  marypha1lem  7965  supmo  7984  suplub2  7993  infmo  8029  ordtypelem3  8053  ordtypelem9  8059  wemaplem1  8079  brwdom3  8115  unwdomg  8117  cantnf  8216  trcl  8230  infxpenc2  8471  aceq2  8568  dfac5lem4  8575  kmlem9  8606  kmlem14  8611  fin23lem26  8773  fin1a2lem13  8860  axdc3lem3  8900  winainflem  9136  axgroth4  9275  suprlub  10593  supaddc  10596  supadd  10597  supmul1  10598  supmullem1  10599  supmullem2  10600  supmul  10601  ublbneg  11271  zsupss  11276  xrsupsslem  11617  xrinfmsslem  11618  fsuppmapnn0fiub  12241  rexanre  13486  rexuzre  13492  rexico  13493  caurcvg2  13821  caucvgb  13823  summolem2  13859  summo  13860  mertens  14019  prodmolem2  14066  prodmo  14067  odd2np1lem  14442  gcdcllem1  14552  pceu  14875  4sqlem12  14979  vdwlem10  15019  vdwlem13  15022  vdwnn  15027  drsdirfi  16261  gaorb  17039  psgnunilem3  17215  psgnunilem4  17216  psgneu  17225  pj1eu  17424  efgsfo  17467  cyggeninv  17596  cygabl  17603  pgpfac1lem5  17790  pgpfac1  17791  pgpfaclem2  17793  lss1d  18264  lspsneq  18423  lspsolvlem  18443  lbsextlem2  18460  mplcoe5lem  18768  cygznlem3  19217  pmatcollpw3fi1lem2  19888  ordtrest2lem  20296  cnprest  20382  1stcfb  20537  1stcelcls  20553  elpt  20664  fbssfi  20930  fgcl  20971  rnelfmlem  21045  fmfnfmlem3  21049  txflf  21099  alexsubb  21139  alexsubALTlem4  21143  isucn2  21372  icccmplem2  21919  ply1divex  23166  coeeu  23258  plydivex  23329  aannenlem2  23364  ulmcau  23429  ulmbdd  23432  dchrptlem2  24272  bposlem9  24299  pntibndlem3  24509  pntlemi  24521  pntlemp  24527  pntleml  24528  pnt3  24529  legval  24708  legov  24709  legov2  24710  outpasch  24876  lnopp2hpgb  24884  colopp  24890  erclwwlksym  25621  erclwwlktr  25622  erclwwlknsym  25633  erclwwlkntr  25634  eleclclwwlkn  25640  hashecclwwlkn1  25641  usghashecclwwlk  25642  frgraregorufr0  25859  isgrpo2  26006  grpoidinvlem3  26015  isgrp2d  26044  isgrpda  26106  ubthlem3  26595  norm1exi  26984  pjhthmo  27036  cdjreui  28166  cdj3i  28175  infxrge0glb  28423  infxrge0glbOLD  28424  isarchi3  28578  archiabl  28589  ordtrest2NEWlem  28802  lmxrge0  28832  esumcvg  28981  esum2d  28988  eulerpartlems  29266  eulerpartlemgvv  29282  conpcon  30030  cvmlift2lem12  30109  cvmlift2lem13  30110  cvmlift3lem2  30115  cvmlift3lem7  30120  cvmlift3  30123  poseq  30562  soseq  30563  funtransport  30869  funray  30978  funline  30980  fnessref  31084  neibastop2  31088  dissneqlem  31812  dissneq  31813  ptrest  32003  poimirlem27  32031  poimirlem32  32036  ismblfin  32045  volsupnfl  32049  itg2addnclem  32057  unirep  32103  filbcmb  32131  sdclem1  32136  sdc  32137  fdc  32138  incsequz  32141  heibor1lem  32205  heiborlem10  32216  isdrngo2  32261  prnc  32364  prtlem13  32504  prtlem15  32511  lshpsmreu  32746  lshpkrlem1  32747  lshpkrlem3  32749  pclfinN  33536  4atex  33712  dihglblem2N  34933  lcfl7N  35140  lcf1o  35190  mzpcompact2lem  35664  eldioph3  35679  diophrex  35689  rexrabdioph  35708  eldioph4i  35726  aomclem8  35990  hbtlem2  36054  rngunsnply  36110  iunrelexpuztr  36382  dvconstbi  36753  expgrowth  36754  wessf1ornlem  37530  limcperiod  37805  limsupre  37818  limsupreOLD  37819  cncfshiftioo  37867  itgiccshift  37954  itgperiod  37955  fourierdlem42  38124  fourierdlem42OLD  38125  fourierdlem48  38130  fourierdlem81  38163  fourierdlem92  38174  fourierdlem96  38178  fourierdlem97  38179  fourierdlem98  38180  fourierdlem99  38181  fourierdlem105  38187  fourierdlem108  38190  fourierdlem110  38192  fourierdlem112  38194  fourierdlem113  38195  hoidmvval0  38527  ovnhoi  38543  ovolval5lem3  38594  ovolval5  38595  2zlidl  40442  2zrngamgm  40447  2zrngagrp  40451  2zrngmmgm  40454
  Copyright terms: Public domain W3C validator