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  6589  eroveu  6904  erovlem  6905  xpf1o  7148  genprndl  7894  genprndu  7895  ltpopr  7968  ltsopr  7969  cauappcvgprlemdisj  8024  caucvgprlemdisj  8047  caucvgprprlemdisj  8075  exbtwnzlemex  10701  rebtwn2z  10706  rexanre  12009  summodc  12175  prodmodclem2  12369  prodmodc  12370  dvds2lem  12595  odd2np1  12665  opoe  12687  omoe  12688  opeo  12689  omeo  12690  gcddiv  12821  divgcdcoprmex  12905  pcqmul  13111  pcadd  13148  mul4sq  13202  4sqlem12  13210  dvdsrtr  14517  unitgrp  14532  lss1d  14829  znidom  15101  tgcl  15290  restbasg  15394  txuni2  15482  txbas  15484  txcnp  15497  blin2  15658  tgqioo  15781  plyadd  15977  plymul  15978  mul2sq  16440  2sqlem5  16443  uhgr2edg  16652