Theorem reeanv 2721

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   E.wrex 2529

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534

This theorem is used by:  3reeanv  2722  fliftfun  6002  tfrlem5  6585  eroveu  6900  erovlem  6901  xpf1o  7144  genprndl  7888  genprndu  7889  ltpopr  7962  ltsopr  7963  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  exbtwnzlemex  10684  rebtwn2z  10689  rexanre  11986  summodc  12150  prodmodclem2  12344  prodmodc  12345  dvds2lem  12570  odd2np1  12640  opoe  12662  omoe  12663  opeo  12664  omeo  12665  gcddiv  12796  divgcdcoprmex  12880  pcqmul  13082  pcadd  13119  mul4sq  13173  4sqlem12  13181  dvdsrtr  14408  unitgrp  14423  lss1d  14720  znidom  14992  tgcl  15165  restbasg  15269  txuni2  15357  txbas  15359  txcnp  15372  blin2  15533  tgqioo  15656  plyadd  15852  plymul  15853  mul2sq  16235  2sqlem5  16238  uhgr2edg  16447