Theorem reeanv 2713

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

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

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526

This theorem is referenced by:  3reeanv  2714  fliftfun  5969  tfrlem5  6545  eroveu  6860  erovlem  6861  xpf1o  7097  genprndl  7836  genprndu  7837  ltpopr  7910  ltsopr  7911  cauappcvgprlemdisj  7966  caucvgprlemdisj  7989  caucvgprprlemdisj  8017  exbtwnzlemex  10609  rebtwn2z  10614  rexanre  11905  summodc  12069  prodmodclem2  12263  prodmodc  12264  dvds2lem  12489  odd2np1  12559  opoe  12581  omoe  12582  opeo  12583  omeo  12584  gcddiv  12715  divgcdcoprmex  12799  pcqmul  13001  pcadd  13038  mul4sq  13092  4sqlem12  13100  dvdsrtr  14246  unitgrp  14261  lss1d  14531  znidom  14805  tgcl  14929  restbasg  15033  txuni2  15121  txbas  15123  txcnp  15136  blin2  15297  tgqioo  15420  plyadd  15616  plymul  15617  mul2sq  15989  2sqlem5  15992  uhgr2edg  16201