Theorem reeanv 3213

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 3212	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3052  df-rex 3061

This theorem is referenced by:  3reeanv  3214  2ralorOLD  3216  2reu4lem  4497  disjxiun  5116  fliftfun  7304  poseq  8155  soseq  8156  frrlem9  8291  tfrlem5  8392  uniinqs  8809  eroveu  8824  erovlem  8825  xpf1o  9151  unxpdomlem3  9258  finsschain  9369  dffi3  9441  ttrcltr  9728  rankxplim3  9893  xpnum  9963  kmlem9  10171  sornom  10289  fpwwe2lem11  10653  cnegex  11414  zaddcl  12630  rexanre  15363  o1lo1  15551  o1co  15600  rlimcn3  15604  o1of2  15627  lo1add  15641  lo1mul  15642  summo  15731  ntrivcvgmul  15916  prodmolem2  15949  prodmo  15950  dvds2lem  16286  odd2np1  16358  opoe  16380  omoe  16381  opeo  16382  omeo  16383  bezoutlem4  16559  gcddiv  16568  divgcdcoprmex  16683  pcqmul  16871  pcadd  16907  mul4sq  16972  4sqlem12  16974  prmgaplem7  17075  cyccom  19184  gaorber  19289  psgneu  19485  lsmsubm  19632  pj1eu  19675  efgredlem  19726  efgrelexlemb  19729  qusabl  19844  dprdsubg  20005  dvdsrtr  20326  unitgrp  20341  lss1d  20918  lsmspsn  21040  lspsolvlem  21101  lbsextlem2  21118  znfld  21519  cygznlem3  21528  psgnghm  21538  tgcl  22905  restbas  23094  ordtbas2  23127  uncmp  23339  txuni2  23501  txbas  23503  ptbasin  23513  txcnp  23556  txlly  23572  txnlly  23573  tx1stc  23586  tx2ndc  23587  fbasrn  23820  rnelfmlem  23888  fmfnfmlem3  23892  txflf  23942  qustgplem  24057  trust  24166  utoptop  24171  fmucndlem  24227  blin2  24366  metustto  24490  tgqioo  24737  minveclem3b  25378  pmltpc  25401  evthicc2  25411  ovolunlem2  25449  dyaddisj  25547  rolle  25944  dvcvx  25975  itgsubst  26006  plyadd  26172  plymul  26173  coeeu  26180  aalioulem6  26295  dchrptlem2  27226  lgsdchr  27316  mul2sq  27380  2sqlem5  27383  pntibnd  27554  pntlemp  27571  nosupprefixmo  27662  noinfprefixmo  27663  addsproplem2  27920  negsproplem2  27978  mulsuniflem  28092  precsexlem10  28157  zaddscl  28297  zmulscld  28300  zseo  28323  recut  28345  readdscl  28348  remulscl  28351  cgraswap  28745  cgracom  28747  cgratr  28748  flatcgra  28749  dfcgra2  28755  acopyeu  28759  ax5seg  28863  axpasch  28866  axeuclid  28888  axcontlem4  28892  axcontlem9  28897  uhgr2edg  29133  2pthon3v  29871  pjhthmo  31229  superpos  32281  chirredi  32321  cdjreui  32359  cdj3i  32368  xrofsup  32690  archiabllem2c  33139  ccfldextdgrr  33659  ordtconnlem1  33901  dya2iocnrect  34259  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  36341  mblfinlem3  37629  ismblfin  37631  itg2addnc  37644  ftc1anclem6  37668  heibor1lem  37779  crngohomfo  37976  ispridlc  38040  prter1  38843  hl2at  39370  cdlemn11pre  41175  dihord2pre  41190  dihord4  41223  dihmeetlem20N  41291  mapdpglem32  41670  diophin  42742  diophun  42743  iunrelexpuztr  43690  mullimc  45593  mullimcf  45600  addlimc  45625  fourierdlem42  46126  fourierdlem80  46163  sge0resplit  46383  hoiqssbllem3  46601