Theorem reeanv 3211

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

Syntax hints:   ↔ wb 207   ∧ wa 396   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3054  df-rex 3064

This theorem is referenced by:  3reeanv  3212  2reu4lem  4452  disjxiun  5070  fliftfun  7257  poseq  8099  soseq  8100  frrlem9  8235  tfrlem5  8310  uniinqs  8735  eroveu  8750  erovlem  8751  xpf1o  9068  unxpdomlem3  9159  finsschain  9260  dffi3  9335  ttrcltr  9629  rankxplim3  9797  xpnum  9867  kmlem9  10073  sornom  10191  fpwwe2lem11  10556  cnegex  11319  zaddcl  12559  rexanre  15301  o1lo1  15491  o1co  15540  rlimcn3  15544  o1of2  15567  lo1add  15581  lo1mul  15582  summo  15671  ntrivcvgmul  15859  prodmolem2  15892  prodmo  15893  dvds2lem  16229  odd2np1  16302  opoe  16324  omoe  16325  opeo  16326  omeo  16327  bezoutlem4  16503  gcddiv  16512  divgcdcoprmex  16627  pcqmul  16816  pcadd  16852  mul4sq  16917  4sqlem12  16919  prmgaplem7  17020  cyccom  19170  gaorber  19275  psgneu  19473  lsmsubm  19620  pj1eu  19663  efgredlem  19714  efgrelexlemb  19717  qusabl  19832  dprdsubg  19993  dvdsrtr  20340  unitgrp  20355  lss1d  20954  lsmspsn  21075  lspsolvlem  21136  lbsextlem2  21153  znfld  21536  cygznlem3  21545  psgnghm  21556  tgcl  22953  restbas  23142  ordtbas2  23175  uncmp  23387  txuni2  23549  txbas  23551  ptbasin  23561  txcnp  23604  txlly  23620  txnlly  23621  tx1stc  23634  tx2ndc  23635  fbasrn  23868  rnelfmlem  23936  fmfnfmlem3  23940  txflf  23990  qustgplem  24105  trust  24213  utoptop  24218  fmucndlem  24274  blin2  24413  metustto  24537  tgqioo  24784  minveclem3b  25414  pmltpc  25436  evthicc2  25446  ovolunlem2  25484  dyaddisj  25582  rolle  25976  dvcvx  26006  itgsubst  26035  plyadd  26201  plymul  26202  coeeu  26209  aalioulem6  26322  dchrptlem2  27247  lgsdchr  27337  mul2sq  27401  2sqlem5  27404  pntibnd  27575  pntlemp  27592  nosupprefixmo  27683  noinfprefixmo  27684  addsproplem2  27981  negsproplem2  28040  mulsuniflem  28160  precsexlem10  28227  zaddscl  28405  zmulscld  28408  zseo  28433  z12addscl  28488  recut  28505  readdscl  28510  remulscl  28513  cgraswap  28907  cgracom  28909  cgratr  28910  flatcgra  28911  dfcgra2  28917  acopyeu  28921  ax5seg  29026  axpasch  29029  axeuclid  29051  axcontlem4  29055  axcontlem9  29060  uhgr2edg  29296  2pthon3v  30030  pjhthmo  31392  superpos  32444  chirredi  32484  cdjreui  32522  cdj3i  32531  xrofsup  32860  archiabllem2c  33277  ccfldextdgrr  33865  ordtconnlem1  34117  dya2iocnrect  34474  txpconn  35469  cvmlift2lem10  35549  cvmlift3lem7  35562  msubco  35768  mclsppslem  35820  altopelaltxp  36213  funtransport  36268  btwnconn1lem13  36336  btwnconn1lem14  36337  segletr  36351  segleantisym  36352  funray  36377  funline  36379  tailfb  36614  mblfinlem3  38035  ismblfin  38037  itg2addnc  38050  ftc1anclem6  38074  heibor1lem  38185  crngohomfo  38382  ispridlc  38446  prter1  39380  hl2at  39906  cdlemn11pre  41711  dihord2pre  41726  dihord4  41759  dihmeetlem20N  41827  mapdpglem32  42206  diophin  43230  diophun  43231  iunrelexpuztr  44172  mullimc  46069  mullimcf  46076  addlimc  46099  fourierdlem42  46600  fourierdlem80  46637  sge0resplit  46857  hoiqssbllem3  47075