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

Theorem reeanv 2741
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 1610 . 2  |-  F/ y
ph
2 nfv 1610 . 2  |-  F/ x ps
31, 2reean 2740 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 2578
This theorem is referenced by:  3reeanv  2742  2ralor  2743  disjxiun  4057  fliftfun  5853  tfrlem5  6438  uniinqs  6781  eroveu  6796  erovlem  6797  xpf1o  7066  unxpdomlem3  7112  unfi  7169  finsschain  7207  dffi3  7229  rankxplim3  7596  xpnum  7629  kmlem9  7829  sornom  7948  fpwwe2lem12  8308  cnegex  9038  zaddcl  10106  rexanre  11877  o1lo1  12058  o1co  12107  rlimcn2  12111  o1of2  12133  lo1add  12147  lo1mul  12148  summo  12237  dvds2lem  12588  odd2np1  12634  bezoutlem4  12767  gcddiv  12775  opoe  12911  omoe  12912  opeo  12913  omeo  12914  pcqmul  12953  pcadd  12984  mul4sq  13048  4sqlem12  13050  gaorber  14811  lsmsubm  15013  pj1eu  15054  efgredlem  15105  efgrelexlemb  15108  divsabl  15206  cygabl  15226  dprdsubg  15308  dvdsrtr  15483  unitgrp  15498  lss1d  15769  lsmspsn  15886  lspsolvlem  15944  lbsextlem2  15961  znfld  16570  cygznlem3  16579  tgcl  16763  restbas  16945  ordtbas2  16977  uncmp  17186  txuni2  17316  txbas  17318  ptbasin  17328  txcnp  17370  txlly  17386  txnlly  17387  tx1stc  17400  tx2ndc  17401  fbasrn  17631  rnelfmlem  17699  fmfnfmlem3  17703  txflf  17753  divstgplem  17855  blin2  18027  tgqioo  18358  minveclem3b  18845  pmltpc  18863  evthicc2  18873  ovolunlem2  18910  dyaddisj  19004  rolle  19390  dvcvx  19420  itgsubst  19449  plyadd  19652  plymul  19653  coeeu  19660  aalioulem6  19770  dchrptlem2  20557  lgsdchr  20640  mul2sq  20657  2sqlem5  20660  pntibnd  20795  pntlemp  20812  pjhthmo  21936  superpos  22989  chirredi  23029  cdjreui  23067  cdj3i  23076  xrofsup  23272  trust  23441  utoptop  23446  fmucndlem  23483  metustto  23495  dya2iocnrect  23805  txpcon  24047  cvmlift2lem10  24127  cvmlift3lem7  24140  ghomgrpilem2  24277  ntrivcvgmul  24407  prodmolem2  24438  prodmo  24439  poseq  24638  soseq  24639  altopelaltxp  24896  ax5seg  24952  axpasch  24955  axeuclid  24977  axcontlem4  24981  axcontlem9  24986  funtransport  25040  btwnconn1lem13  25108  btwnconn1lem14  25109  segletr  25123  segleantisym  25124  funray  25149  funline  25151  itg2addnc  25319  tailfb  25475  heibor1lem  25681  crngohomfo  25779  ispridlc  25843  prter1  25895  diophin  26000  diophun  26001  psgneu  26577  psgnghm  26585  2reu4a  27115  usgra2edg  27353  hl2at  29412  cdlemn11pre  31218  dihord2pre  31233  dihord4  31266  dihmeetlem20N  31334  mapdpglem32  31713
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583
  Copyright terms: Public domain W3C validator