Theorem reeanv 2893

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

Step	Hyp	Ref	Expression
1		nfv 1673	. 2 |- F/ y ph
2		nfv 1673	. 2 |- F/ x ps
3	1, 2	reean 2892	1 |- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Syntax hints:   <-> wb 184   /\ wa 369   E.wrex 2721

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rex 2726

This theorem is referenced by:  3reeanv  2894  2ralor  2895  disjxiun  4294  fliftfun  6010  tfrlem5  6844  uniinqs  7185  eroveu  7200  erovlem  7201  xpf1o  7478  unxpdomlem3  7524  unfi  7584  finsschain  7623  dffi3  7686  rankxplim3  8093  xpnum  8126  kmlem9  8332  sornom  8451  fpwwe2lem12  8813  cnegex  9555  zaddcl  10690  rexanre  12839  o1lo1  13020  o1co  13069  rlimcn2  13073  o1of2  13095  lo1add  13109  lo1mul  13110  summo  13199  dvds2lem  13550  odd2np1  13597  bezoutlem4  13730  gcddiv  13738  opoe  13883  omoe  13884  opeo  13885  omeo  13886  pcqmul  13925  pcadd  13956  mul4sq  14020  4sqlem12  14022  gaorber  15831  psgneu  16017  lsmsubm  16157  pj1eu  16198  efgredlem  16249  efgrelexlemb  16252  divsabl  16352  cygabl  16372  dprdsubg  16526  dvdsrtr  16749  unitgrp  16764  lss1d  17049  lsmspsn  17170  lspsolvlem  17228  lbsextlem2  17245  znfld  17998  cygznlem3  18007  psgnghm  18015  tgcl  18579  restbas  18767  ordtbas2  18800  uncmp  19011  txuni2  19143  txbas  19145  ptbasin  19155  txcnp  19198  txlly  19214  txnlly  19215  tx1stc  19228  tx2ndc  19229  fbasrn  19462  rnelfmlem  19530  fmfnfmlem3  19534  txflf  19584  divstgplem  19696  trust  19809  utoptop  19814  fmucndlem  19871  blin2  20009  metusttoOLD  20137  metustto  20138  tgqioo  20382  minveclem3b  20920  pmltpc  20939  evthicc2  20949  ovolunlem2  20986  dyaddisj  21081  rolle  21467  dvcvx  21497  itgsubst  21526  plyadd  21690  plymul  21691  coeeu  21698  aalioulem6  21808  dchrptlem2  22609  lgsdchr  22692  mul2sq  22709  2sqlem5  22712  pntibnd  22847  pntlemp  22864  ax5seg  23189  axpasch  23192  axeuclid  23214  axcontlem4  23218  axcontlem9  23223  usgra2edg  23306  pjhthmo  24710  superpos  25763  chirredi  25803  cdjreui  25841  cdj3i  25850  xrofsup  26060  archiabllem2c  26217  ordtconlem1  26359  dya2iocnrect  26701  txpcon  27126  cvmlift2lem10  27206  cvmlift3lem7  27219  ghomgrpilem2  27310  ntrivcvgmul  27422  prodmolem2  27453  prodmo  27454  poseq  27719  soseq  27720  altopelaltxp  28012  funtransport  28067  btwnconn1lem13  28135  btwnconn1lem14  28136  segletr  28150  segleantisym  28151  funray  28176  funline  28178  mblfinlem3  28435  ismblfin  28437  itg2addnc  28451  ftc1anclem6  28477  tailfb  28603  heibor1lem  28713  crngohomfo  28811  ispridlc  28875  prter1  29029  diophin  29116  diophun  29117  2reu4a  30018  frgrawopreglem5  30646  hl2at  33054  cdlemn11pre  34860  dihord2pre  34875  dihord4  34908  dihmeetlem20N  34976  mapdpglem32  35355