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

Theorem reeanv 2707
Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)
Assertion
Ref Expression
reeanv  |-  ( E. x  e.  A  E. y  e.  B  ( ph  /\  ps )  <->  ( E. x  e.  A  ph  /\  E. y  e.  B  ps ) )
Distinct variable groups:    ph, y    ps, x    x, y    y, A   
x, B
Allowed substitution hints:    ph( x)    ps( y)    A( x)    B( y)

Proof of Theorem reeanv
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ y
ph
2 nfv 1605 . 2  |-  F/ x ps
31, 2reean 2706 1  |-  ( E. x  e.  A  E. y  e.  B  ( ph  /\  ps )  <->  ( E. x  e.  A  ph  /\  E. y  e.  B  ps ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wrex 2544
This theorem is referenced by:  3reeanv  2708  2ralor  2709  disjxiun  4020  fliftfun  5811  tfrlem5  6396  eroveu  6753  erovlem  6754  xpf1o  7023  unxpdomlem3  7069  unfi  7124  finsschain  7162  dffi3  7184  rankxplim3  7551  xpnum  7584  kmlem9  7784  sornom  7903  fpwwe2lem12  8263  cnegex  8993  zaddcl  10059  rexanre  11830  o1lo1  12011  o1co  12060  rlimcn2  12064  o1of2  12086  lo1add  12100  lo1mul  12101  summo  12190  dvds2lem  12541  odd2np1  12587  bezoutlem4  12720  gcddiv  12728  opoe  12864  omoe  12865  opeo  12866  omeo  12867  pcqmul  12906  pcadd  12937  mul4sq  13001  4sqlem12  13003  gaorber  14762  lsmsubm  14964  pj1eu  15005  efgredlem  15056  efgrelexlemb  15059  divsabl  15157  cygabl  15177  dprdsubg  15259  dvdsrtr  15434  unitgrp  15449  lss1d  15720  lsmspsn  15837  lspsolvlem  15895  lbsextlem2  15912  znfld  16514  cygznlem3  16523  tgcl  16707  restbas  16889  ordtbas2  16921  uncmp  17130  txuni2  17260  txbas  17262  ptbasin  17272  txcnp  17314  txlly  17330  txnlly  17331  tx1stc  17344  tx2ndc  17345  fbasrn  17579  rnelfmlem  17647  fmfnfmlem3  17651  txflf  17701  divstgplem  17803  blin2  17975  tgqioo  18306  minveclem3b  18792  pmltpc  18810  evthicc2  18820  ovolunlem2  18857  dyaddisj  18951  rolle  19337  dvcvx  19367  itgsubst  19396  plyadd  19599  plymul  19600  coeeu  19607  aalioulem6  19717  dchrptlem2  20504  lgsdchr  20587  mul2sq  20604  2sqlem5  20607  pntibnd  20742  pntlemp  20759  pjhthmo  21881  superpos  22934  chirredi  22974  cdjreui  23012  cdj3i  23021  xrofsup  23255  txpcon  23763  cvmlift2lem10  23843  cvmlift3lem7  23856  ghomgrpilem2  23993  poseq  24253  soseq  24254  altopelaltxp  24510  ax5seg  24566  axpasch  24569  axeuclid  24591  axcontlem4  24595  axcontlem9  24600  funtransport  24654  btwnconn1lem13  24722  btwnconn1lem14  24723  segletr  24737  segleantisym  24738  funray  24763  funline  24765  uninqs  25039  tailfb  26326  heibor1lem  26533  crngohomfo  26631  ispridlc  26695  prter1  26747  diophin  26852  diophun  26853  psgneu  27429  psgnghm  27437  2reu4a  27967  hl2at  29594  cdlemn11pre  31400  dihord2pre  31415  dihord4  31448  dihmeetlem20N  31516  mapdpglem32  31895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549
  Copyright terms: Public domain W3C validator