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  6002  tfrlem5  6585  eroveu  6900  erovlem  6901  xpf1o  7144  genprndl  7888  genprndu  7889  ltpopr  7962  ltsopr  7963  cauappcvgprlemdisj  8018  caucvgprlemdisj  8041  caucvgprprlemdisj  8069  exbtwnzlemex  10694  rebtwn2z  10699  rexanre  12001  summodc  12166  prodmodclem2  12360  prodmodc  12361  dvds2lem  12586  odd2np1  12656  opoe  12678  omoe  12679  opeo  12680  omeo  12681  gcddiv  12812  divgcdcoprmex  12896  pcqmul  13102  pcadd  13139  mul4sq  13193  4sqlem12  13201  dvdsrtr  14457  unitgrp  14472  lss1d  14769  znidom  15041  tgcl  15214  restbasg  15318  txuni2  15406  txbas  15408  txcnp  15421  blin2  15582  tgqioo  15705  plyadd  15901  plymul  15902  mul2sq  16333  2sqlem5  16336  uhgr2edg  16545