Theorem reeanv 2701

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

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

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514

This theorem is referenced by:  3reeanv  2702  fliftfun  5926  tfrlem5  6466  eroveu  6781  erovlem  6782  xpf1o  7013  genprndl  7719  genprndu  7720  ltpopr  7793  ltsopr  7794  cauappcvgprlemdisj  7849  caucvgprlemdisj  7872  caucvgprprlemdisj  7900  exbtwnzlemex  10481  rebtwn2z  10486  rexanre  11746  summodc  11909  prodmodclem2  12103  prodmodc  12104  dvds2lem  12329  odd2np1  12399  opoe  12421  omoe  12422  opeo  12423  omeo  12424  gcddiv  12555  divgcdcoprmex  12639  pcqmul  12841  pcadd  12878  mul4sq  12932  4sqlem12  12940  dvdsrtr  14080  unitgrp  14095  lss1d  14362  znidom  14636  tgcl  14753  restbasg  14857  txuni2  14945  txbas  14947  txcnp  14960  blin2  15121  tgqioo  15244  plyadd  15440  plymul  15441  mul2sq  15810  2sqlem5  15813  uhgr2edg  16019