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  5929  tfrlem5  6471  eroveu  6786  erovlem  6787  xpf1o  7018  genprndl  7724  genprndu  7725  ltpopr  7798  ltsopr  7799  cauappcvgprlemdisj  7854  caucvgprlemdisj  7877  caucvgprprlemdisj  7905  exbtwnzlemex  10486  rebtwn2z  10491  rexanre  11752  summodc  11915  prodmodclem2  12109  prodmodc  12110  dvds2lem  12335  odd2np1  12405  opoe  12427  omoe  12428  opeo  12429  omeo  12430  gcddiv  12561  divgcdcoprmex  12645  pcqmul  12847  pcadd  12884  mul4sq  12938  4sqlem12  12946  dvdsrtr  14086  unitgrp  14101  lss1d  14368  znidom  14642  tgcl  14759  restbasg  14863  txuni2  14951  txbas  14953  txcnp  14966  blin2  15127  tgqioo  15250  plyadd  15446  plymul  15447  mul2sq  15816  2sqlem5  15819  uhgr2edg  16025