Theorem reeanv 2667

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

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

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481

This theorem is referenced by:  3reeanv  2668  fliftfun  5843  tfrlem5  6372  eroveu  6685  erovlem  6686  xpf1o  6905  genprndl  7588  genprndu  7589  ltpopr  7662  ltsopr  7663  cauappcvgprlemdisj  7718  caucvgprlemdisj  7741  caucvgprprlemdisj  7769  exbtwnzlemex  10339  rebtwn2z  10344  rexanre  11385  summodc  11548  prodmodclem2  11742  prodmodc  11743  dvds2lem  11968  odd2np1  12038  opoe  12060  omoe  12061  opeo  12062  omeo  12063  gcddiv  12186  divgcdcoprmex  12270  pcqmul  12472  pcadd  12509  mul4sq  12563  4sqlem12  12571  dvdsrtr  13657  unitgrp  13672  lss1d  13939  znidom  14213  tgcl  14300  restbasg  14404  txuni2  14492  txbas  14494  txcnp  14507  blin2  14668  tgqioo  14791  plyadd  14987  plymul  14988  mul2sq  15357  2sqlem5  15360