Theorem reeanv 3237

Description: Rearrange restricted 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		exdistrv 1985	. 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓)))
2	1	reeanlem 3236	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  3reeanv  3238  2reu4lem  4484  disjxiun  5106  fliftfun  7310  poseq  8150  soseq  8151  frrlem9  8287  tfrlem5  8362  uniinqs  8791  eroveu  8806  erovlem  8807  xpf1o  9123  unxpdomlem3  9214  finsschain  9312  dffi3  9387  ttrcltr  9681  rankxplim3  9849  xpnum  9933  kmlem9  10138  sornom  10256  fpwwe2lem11  10621  cnegex  11386  zaddcl  12629  rexanre  15394  o1lo1  15584  o1co  15633  rlimcn3  15637  o1of2  15660  lo1add  15674  lo1mul  15675  summo  15764  ntrivcvgmul  15952  prodmolem2  15985  prodmo  15986  dvds2lem  16321  odd2np1  16394  opoe  16416  omoe  16417  opeo  16418  omeo  16419  bezoutlem4  16595  gcddiv  16604  divgcdcoprmex  16719  pcqmul  16908  pcadd  16944  mul4sq  17009  4sqlem12  17011  prmgaplem7  17112  cyccom  19269  gaorber  19373  psgneu  19571  lsmsubm  19718  pj1eu  19761  efgredlem  19812  efgrelexlemb  19815  qusabl  19930  dprdsubg  20091  dvdsrtr  20446  unitgrp  20461  crngrhmfo  20574  lss1d  21084  lsmspsn  21205  lspsolvlem  21266  lbsextlem2  21283  znfld  21710  cygznlem3  21719  psgnghm  21730  tgcl  23126  restbas  23315  ordtbas2  23348  uncmp  23560  txuni2  23722  txbas  23724  ptbasin  23734  txcnp  23777  txlly  23793  txnlly  23794  tx1stc  23807  tx2ndc  23808  fbasrn  24041  rnelfmlem  24109  fmfnfmlem3  24113  txflf  24163  qustgplem  24278  trust  24386  utoptop  24391  fmucndlem  24447  blin2  24586  metustto  24710  tgqioo  24957  minveclem3b  25587  pmltpc  25609  evthicc2  25619  ovolunlem2  25657  dyaddisj  25755  rolle  26149  dvcvx  26179  itgsubst  26208  plyadd  26374  plymul  26375  coeeu  26382  aalioulem6  26500  dchrptlem2  27429  lgsdchr  27519  mul2sq  27583  2sqlem5  27586  pntibnd  27757  pntlemp  27774  nosupprefixmo  27864  noinfprefixmo  27865  addsproplem2  28163  negsproplem2  28222  mulsuniflem  28342  precsexlem10  28409  zaddscl  28587  zmulscld  28590  zseo  28615  z12addscl  28670  recut  28687  readdscl  28692  remulscl  28695  cgraswap  29131  cgracom  29133  cgratr  29134  flatcgra  29135  dfcgra2  29141  acopyeu  29145  ax5seg  29288  axpasch  29291  axeuclid  29313  axcontlem4  29317  axcontlem9  29322  uhgr2edg  29558  2pthon3v  30292  pjhthmo  31654  superpos  32706  chirredi  32746  cdjreui  32784  cdj3i  32793  xrofsup  33112  archiabllem2c  33515  ccfldextdgrr  34062  ordtconnlem1  34314  dya2iocnrect  34671  txpconn  35724  cvmlift2lem10  35804  cvmlift3lem7  35817  msubco  36023  mclsppslem  36075  altopelaltxp  36468  funtransport  36523  btwnconn1lem13  36591  btwnconn1lem14  36592  segletr  36606  segleantisym  36607  funray  36632  funline  36634  tailfb  36908  mblfinlem3  38330  ismblfin  38332  itg2addnc  38345  ftc1anclem6  38369  heibor1lem  38480  crngohomfo  38677  ispridlc  38741  prter1  39673  hl2at  40199  cdlemn11pre  42004  dihord2pre  42019  dihord4  42052  dihmeetlem20N  42120  mapdpglem32  42499  diophin  43523  diophun  43524  iunrelexpuztr  44465  mullimc  46352  mullimcf  46359  addlimc  46382  fourierdlem42  46883  fourierdlem80  46920  sge0resplit  47140  hoiqssbllem3  47358