Theorem reeanv 3235

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 1955	. 2 ⊢ (∃𝑥∃𝑦((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐵 ∧ 𝜓)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∃𝑦(𝑦 ∈ 𝐵 ∧ 𝜓)))
2	1	reeanlem 3234	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  3reeanv  3236  2ralorOLD  3238  2reu4lem  4545  disjxiun  5163  fliftfun  7348  poseq  8199  soseq  8200  frrlem9  8335  tfrlem5  8436  uniinqs  8855  eroveu  8870  erovlem  8871  xpf1o  9205  unxpdomlem3  9315  finsschain  9429  dffi3  9500  ttrcltr  9785  rankxplim3  9950  xpnum  10020  kmlem9  10228  sornom  10346  fpwwe2lem11  10710  cnegex  11471  zaddcl  12683  rexanre  15395  o1lo1  15583  o1co  15632  rlimcn3  15636  o1of2  15659  lo1add  15673  lo1mul  15674  summo  15765  ntrivcvgmul  15950  prodmolem2  15983  prodmo  15984  dvds2lem  16317  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  bezoutlem4  16589  gcddiv  16598  divgcdcoprmex  16713  pcqmul  16900  pcadd  16936  mul4sq  17001  4sqlem12  17003  prmgaplem7  17104  cyccom  19243  gaorber  19348  psgneu  19548  lsmsubm  19695  pj1eu  19738  efgredlem  19789  efgrelexlemb  19792  qusabl  19907  dprdsubg  20068  dvdsrtr  20394  unitgrp  20409  lss1d  20984  lsmspsn  21106  lspsolvlem  21167  lbsextlem2  21184  znfld  21602  cygznlem3  21611  psgnghm  21621  tgcl  22997  restbas  23187  ordtbas2  23220  uncmp  23432  txuni2  23594  txbas  23596  ptbasin  23606  txcnp  23649  txlly  23665  txnlly  23666  tx1stc  23679  tx2ndc  23680  fbasrn  23913  rnelfmlem  23981  fmfnfmlem3  23985  txflf  24035  qustgplem  24150  trust  24259  utoptop  24264  fmucndlem  24321  blin2  24460  metustto  24587  tgqioo  24841  minveclem3b  25481  pmltpc  25504  evthicc2  25514  ovolunlem2  25552  dyaddisj  25650  rolle  26048  dvcvx  26079  itgsubst  26110  plyadd  26276  plymul  26277  coeeu  26284  aalioulem6  26397  dchrptlem2  27327  lgsdchr  27417  mul2sq  27481  2sqlem5  27484  pntibnd  27655  pntlemp  27672  nosupprefixmo  27763  noinfprefixmo  27764  addsproplem2  28021  negsproplem2  28079  mulsuniflem  28193  precsexlem10  28258  zaddscl  28398  zmulscld  28401  zseo  28424  recut  28446  readdscl  28449  remulscl  28452  cgraswap  28846  cgracom  28848  cgratr  28849  flatcgra  28850  dfcgra2  28856  acopyeu  28860  ax5seg  28971  axpasch  28974  axeuclid  28996  axcontlem4  29000  axcontlem9  29005  uhgr2edg  29243  2pthon3v  29976  pjhthmo  31334  superpos  32386  chirredi  32426  cdjreui  32464  cdj3i  32473  xrofsup  32774  archiabllem2c  33175  ccfldextdgrr  33682  ordtconnlem1  33870  dya2iocnrect  34246  txpconn  35200  cvmlift2lem10  35280  cvmlift3lem7  35293  msubco  35499  mclsppslem  35551  altopelaltxp  35940  funtransport  35995  btwnconn1lem13  36063  btwnconn1lem14  36064  segletr  36078  segleantisym  36079  funray  36104  funline  36106  tailfb  36343  mblfinlem3  37619  ismblfin  37621  itg2addnc  37634  ftc1anclem6  37658  heibor1lem  37769  crngohomfo  37966  ispridlc  38030  prter1  38835  hl2at  39362  cdlemn11pre  41167  dihord2pre  41182  dihord4  41215  dihmeetlem20N  41283  mapdpglem32  41662  diophin  42728  diophun  42729  iunrelexpuztr  43681  mullimc  45537  mullimcf  45544  addlimc  45569  fourierdlem42  46070  fourierdlem80  46107  sge0resplit  46327  hoiqssbllem3  46545