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  7889  genprndu  7890  ltpopr  7963  ltsopr  7964  cauappcvgprlemdisj  8019  caucvgprlemdisj  8042  caucvgprprlemdisj  8070  exbtwnzlemex  10695  rebtwn2z  10700  rexanre  12003  summodc  12169  prodmodclem2  12363  prodmodc  12364  dvds2lem  12589  odd2np1  12659  opoe  12681  omoe  12682  opeo  12683  omeo  12684  gcddiv  12815  divgcdcoprmex  12899  pcqmul  13105  pcadd  13142  mul4sq  13196  4sqlem12  13204  dvdsrtr  14492  unitgrp  14507  lss1d  14804  znidom  15076  tgcl  15256  restbasg  15360  txuni2  15448  txbas  15450  txcnp  15463  blin2  15624  tgqioo  15747  plyadd  15943  plymul  15944  mul2sq  16401  2sqlem5  16404  uhgr2edg  16613