Theorem reeanv 2703

Description: Rearrange existential quantifiers. (Contributed by NM, 9-May-1999.)

Assertion

Ref	Expression
reeanv	⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦   𝑦,𝐴   𝑥,𝐵

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝐴(𝑥)   𝐵(𝑦)

Proof of Theorem reeanv

Step	Hyp	Ref	Expression
1		nfv 1576	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1576	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 2702	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wrex 2511

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516

This theorem is referenced by:  3reeanv  2704  fliftfun  5937  tfrlem5  6480  eroveu  6795  erovlem  6796  xpf1o  7030  genprndl  7741  genprndu  7742  ltpopr  7815  ltsopr  7816  cauappcvgprlemdisj  7871  caucvgprlemdisj  7894  caucvgprprlemdisj  7922  exbtwnzlemex  10510  rebtwn2z  10515  rexanre  11798  summodc  11962  prodmodclem2  12156  prodmodc  12157  dvds2lem  12382  odd2np1  12452  opoe  12474  omoe  12475  opeo  12476  omeo  12477  gcddiv  12608  divgcdcoprmex  12692  pcqmul  12894  pcadd  12931  mul4sq  12985  4sqlem12  12993  dvdsrtr  14134  unitgrp  14149  lss1d  14416  znidom  14690  tgcl  14807  restbasg  14911  txuni2  14999  txbas  15001  txcnp  15014  blin2  15175  tgqioo  15298  plyadd  15494  plymul  15495  mul2sq  15864  2sqlem5  15867  uhgr2edg  16076