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  5919  tfrlem5  6458  eroveu  6771  erovlem  6772  xpf1o  7001  genprndl  7704  genprndu  7705  ltpopr  7778  ltsopr  7779  cauappcvgprlemdisj  7834  caucvgprlemdisj  7857  caucvgprprlemdisj  7885  exbtwnzlemex  10464  rebtwn2z  10469  rexanre  11726  summodc  11889  prodmodclem2  12083  prodmodc  12084  dvds2lem  12309  odd2np1  12379  opoe  12401  omoe  12402  opeo  12403  omeo  12404  gcddiv  12535  divgcdcoprmex  12619  pcqmul  12821  pcadd  12858  mul4sq  12912  4sqlem12  12920  dvdsrtr  14059  unitgrp  14074  lss1d  14341  znidom  14615  tgcl  14732  restbasg  14836  txuni2  14924  txbas  14926  txcnp  14939  blin2  15100  tgqioo  15223  plyadd  15419  plymul  15420  mul2sq  15789  2sqlem5  15792  uhgr2edg  15998