Theorem reeanv 2721

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105  ∃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  6005  tfrlem5  6590  eroveu  6905  erovlem  6906  xpf1o  7150  genprndl  7894  genprndu  7895  ltpopr  7968  ltsopr  7969  cauappcvgprlemdisj  8024  caucvgprlemdisj  8047  caucvgprprlemdisj  8075  exbtwnzlemex  10700  rebtwn2z  10705  rexanre  12008  summodc  12174  prodmodclem2  12368  prodmodc  12369  dvds2lem  12594  odd2np1  12664  opoe  12686  omoe  12687  opeo  12688  omeo  12689  gcddiv  12820  divgcdcoprmex  12904  pcqmul  13110  pcadd  13147  mul4sq  13201  4sqlem12  13209  dvdsrtr  14516  unitgrp  14531  lss1d  14828  znidom  15100  tgcl  15307  restbasg  15411  txuni2  15499  txbas  15501  txcnp  15514  blin2  15675  tgqioo  15798  plyadd  15994  plymul  15995  mul2sq  16457  2sqlem5  16460  uhgr2edg  16669