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

Theorem reeanv 2867
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 1629 . 2  |-  F/ y
ph
2 nfv 1629 . 2  |-  F/ x ps
31, 2reean 2866 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 177    /\ wa 359   E.wrex 2698
This theorem is referenced by:  3reeanv  2868  2ralor  2869  disjxiun  4201  fliftfun  6026  tfrlem5  6633  uniinqs  6976  eroveu  6991  erovlem  6992  xpf1o  7261  unxpdomlem3  7307  unfi  7366  finsschain  7405  dffi3  7428  rankxplim3  7797  xpnum  7830  kmlem9  8030  sornom  8149  fpwwe2lem12  8508  cnegex  9239  zaddcl  10309  rexanre  12142  o1lo1  12323  o1co  12372  rlimcn2  12376  o1of2  12398  lo1add  12412  lo1mul  12413  summo  12503  dvds2lem  12854  odd2np1  12900  bezoutlem4  13033  gcddiv  13041  opoe  13177  omoe  13178  opeo  13179  omeo  13180  pcqmul  13219  pcadd  13250  mul4sq  13314  4sqlem12  13316  gaorber  15077  lsmsubm  15279  pj1eu  15320  efgredlem  15371  efgrelexlemb  15374  divsabl  15472  cygabl  15492  dprdsubg  15574  dvdsrtr  15749  unitgrp  15764  lss1d  16031  lsmspsn  16148  lspsolvlem  16206  lbsextlem2  16223  znfld  16833  cygznlem3  16842  tgcl  17026  restbas  17214  ordtbas2  17247  uncmp  17458  txuni2  17589  txbas  17591  ptbasin  17601  txcnp  17644  txlly  17660  txnlly  17661  tx1stc  17674  tx2ndc  17675  fbasrn  17908  rnelfmlem  17976  fmfnfmlem3  17980  txflf  18030  divstgplem  18142  trust  18251  utoptop  18256  fmucndlem  18313  blin2  18451  metusttoOLD  18579  metustto  18580  tgqioo  18823  minveclem3b  19321  pmltpc  19339  evthicc2  19349  ovolunlem2  19386  dyaddisj  19480  rolle  19866  dvcvx  19896  itgsubst  19925  plyadd  20128  plymul  20129  coeeu  20136  aalioulem6  20246  dchrptlem2  21041  lgsdchr  21124  mul2sq  21141  2sqlem5  21144  pntibnd  21279  pntlemp  21296  usgra2edg  21394  pjhthmo  22796  superpos  23849  chirredi  23889  cdjreui  23927  cdj3i  23936  xrofsup  24118  dya2iocnrect  24623  txpcon  24911  cvmlift2lem10  24991  cvmlift3lem7  25004  ghomgrpilem2  25089  ntrivcvgmul  25222  prodmolem2  25253  prodmo  25254  poseq  25520  soseq  25521  altopelaltxp  25813  ax5seg  25869  axpasch  25872  axeuclid  25894  axcontlem4  25898  axcontlem9  25903  funtransport  25957  btwnconn1lem13  26025  btwnconn1lem14  26026  segletr  26040  segleantisym  26041  funray  26066  funline  26068  mblfinlem2  26235  ismblfin  26237  itg2addnc  26249  ftc1anclem6  26275  tailfb  26397  heibor1lem  26509  crngohomfo  26607  ispridlc  26671  prter1  26719  diophin  26822  diophun  26823  psgneu  27397  psgnghm  27405  2reu4a  27934  frgrawopreglem5  28374  hl2at  30139  cdlemn11pre  31945  dihord2pre  31960  dihord4  31993  dihmeetlem20N  32061  mapdpglem32  32440
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703
  Copyright terms: Public domain W3C validator