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  5926  tfrlem5  6466  eroveu  6781  erovlem  6782  xpf1o  7013  genprndl  7719  genprndu  7720  ltpopr  7793  ltsopr  7794  cauappcvgprlemdisj  7849  caucvgprlemdisj  7872  caucvgprprlemdisj  7900  exbtwnzlemex  10481  rebtwn2z  10486  rexanre  11747  summodc  11910  prodmodclem2  12104  prodmodc  12105  dvds2lem  12330  odd2np1  12400  opoe  12422  omoe  12423  opeo  12424  omeo  12425  gcddiv  12556  divgcdcoprmex  12640  pcqmul  12842  pcadd  12879  mul4sq  12933  4sqlem12  12941  dvdsrtr  14081  unitgrp  14096  lss1d  14363  znidom  14637  tgcl  14754  restbasg  14858  txuni2  14946  txbas  14948  txcnp  14961  blin2  15122  tgqioo  15245  plyadd  15441  plymul  15442  mul2sq  15811  2sqlem5  15814  uhgr2edg  16020