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  5936  tfrlem5  6479  eroveu  6794  erovlem  6795  xpf1o  7029  genprndl  7740  genprndu  7741  ltpopr  7814  ltsopr  7815  cauappcvgprlemdisj  7870  caucvgprlemdisj  7893  caucvgprprlemdisj  7921  exbtwnzlemex  10508  rebtwn2z  10513  rexanre  11780  summodc  11943  prodmodclem2  12137  prodmodc  12138  dvds2lem  12363  odd2np1  12433  opoe  12455  omoe  12456  opeo  12457  omeo  12458  gcddiv  12589  divgcdcoprmex  12673  pcqmul  12875  pcadd  12912  mul4sq  12966  4sqlem12  12974  dvdsrtr  14114  unitgrp  14129  lss1d  14396  znidom  14670  tgcl  14787  restbasg  14891  txuni2  14979  txbas  14981  txcnp  14994  blin2  15155  tgqioo  15278  plyadd  15474  plymul  15475  mul2sq  15844  2sqlem5  15847  uhgr2edg  16056