Theorem reeanv 2676

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

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

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490

This theorem is referenced by:  3reeanv  2677  fliftfun  5865  tfrlem5  6400  eroveu  6713  erovlem  6714  xpf1o  6941  genprndl  7634  genprndu  7635  ltpopr  7708  ltsopr  7709  cauappcvgprlemdisj  7764  caucvgprlemdisj  7787  caucvgprprlemdisj  7815  exbtwnzlemex  10392  rebtwn2z  10397  rexanre  11531  summodc  11694  prodmodclem2  11888  prodmodc  11889  dvds2lem  12114  odd2np1  12184  opoe  12206  omoe  12207  opeo  12208  omeo  12209  gcddiv  12340  divgcdcoprmex  12424  pcqmul  12626  pcadd  12663  mul4sq  12717  4sqlem12  12725  dvdsrtr  13863  unitgrp  13878  lss1d  14145  znidom  14419  tgcl  14536  restbasg  14640  txuni2  14728  txbas  14730  txcnp  14743  blin2  14904  tgqioo  15027  plyadd  15223  plymul  15224  mul2sq  15593  2sqlem5  15596