Theorem reeanv 2678

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 1552	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1552	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	reean 2677	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

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

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492

This theorem is referenced by:  3reeanv  2679  fliftfun  5888  tfrlem5  6423  eroveu  6736  erovlem  6737  xpf1o  6966  genprndl  7669  genprndu  7670  ltpopr  7743  ltsopr  7744  cauappcvgprlemdisj  7799  caucvgprlemdisj  7822  caucvgprprlemdisj  7850  exbtwnzlemex  10429  rebtwn2z  10434  rexanre  11646  summodc  11809  prodmodclem2  12003  prodmodc  12004  dvds2lem  12229  odd2np1  12299  opoe  12321  omoe  12322  opeo  12323  omeo  12324  gcddiv  12455  divgcdcoprmex  12539  pcqmul  12741  pcadd  12778  mul4sq  12832  4sqlem12  12840  dvdsrtr  13978  unitgrp  13993  lss1d  14260  znidom  14534  tgcl  14651  restbasg  14755  txuni2  14843  txbas  14845  txcnp  14858  blin2  15019  tgqioo  15142  plyadd  15338  plymul  15339  mul2sq  15708  2sqlem5  15711