Theorem reeanv 2701

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 1574	. 2 |- F/ y ph
2		nfv 1574	. 2 |- F/ x ps
3	1, 2	reean 2700	1 |- ( E. x e. A E. y e. B ( ph /\ ps ) <-> ( E. x e. A ph /\ E. y e. B ps ) )

Syntax hints:   /\ wa 104   <-> wb 105   E.wrex 2509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514

This theorem is referenced by:  3reeanv  2702  fliftfun  5920  tfrlem5  6460  eroveu  6773  erovlem  6774  xpf1o  7005  genprndl  7708  genprndu  7709  ltpopr  7782  ltsopr  7783  cauappcvgprlemdisj  7838  caucvgprlemdisj  7861  caucvgprprlemdisj  7889  exbtwnzlemex  10469  rebtwn2z  10474  rexanre  11731  summodc  11894  prodmodclem2  12088  prodmodc  12089  dvds2lem  12314  odd2np1  12384  opoe  12406  omoe  12407  opeo  12408  omeo  12409  gcddiv  12540  divgcdcoprmex  12624  pcqmul  12826  pcadd  12863  mul4sq  12917  4sqlem12  12925  dvdsrtr  14065  unitgrp  14080  lss1d  14347  znidom  14621  tgcl  14738  restbasg  14842  txuni2  14930  txbas  14932  txcnp  14945  blin2  15106  tgqioo  15229  plyadd  15425  plymul  15426  mul2sq  15795  2sqlem5  15798  uhgr2edg  16004