Theorem reeanv 3208

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  3reeanv  3209  2reu4lem  4476  disjxiun  5095  fliftfun  7258  poseq  8100  soseq  8101  frrlem9  8236  tfrlem5  8311  uniinqs  8736  eroveu  8751  erovlem  8752  xpf1o  9069  unxpdomlem3  9160  finsschain  9261  dffi3  9336  ttrcltr  9627  rankxplim3  9795  xpnum  9865  kmlem9  10071  sornom  10189  fpwwe2lem11  10554  cnegex  11316  zaddcl  12533  rexanre  15272  o1lo1  15462  o1co  15511  rlimcn3  15515  o1of2  15538  lo1add  15552  lo1mul  15553  summo  15642  ntrivcvgmul  15827  prodmolem2  15860  prodmo  15861  dvds2lem  16197  odd2np1  16270  opoe  16292  omoe  16293  opeo  16294  omeo  16295  bezoutlem4  16471  gcddiv  16480  divgcdcoprmex  16595  pcqmul  16783  pcadd  16819  mul4sq  16884  4sqlem12  16886  prmgaplem7  16987  cyccom  19134  gaorber  19239  psgneu  19437  lsmsubm  19584  pj1eu  19627  efgredlem  19678  efgrelexlemb  19681  qusabl  19796  dprdsubg  19957  dvdsrtr  20306  unitgrp  20321  lss1d  20916  lsmspsn  21038  lspsolvlem  21099  lbsextlem2  21116  znfld  21517  cygznlem3  21526  psgnghm  21537  tgcl  22915  restbas  23104  ordtbas2  23137  uncmp  23349  txuni2  23511  txbas  23513  ptbasin  23523  txcnp  23566  txlly  23582  txnlly  23583  tx1stc  23596  tx2ndc  23597  fbasrn  23830  rnelfmlem  23898  fmfnfmlem3  23902  txflf  23952  qustgplem  24067  trust  24175  utoptop  24180  fmucndlem  24236  blin2  24375  metustto  24499  tgqioo  24746  minveclem3b  25386  pmltpc  25409  evthicc2  25419  ovolunlem2  25457  dyaddisj  25555  rolle  25952  dvcvx  25983  itgsubst  26014  plyadd  26180  plymul  26181  coeeu  26188  aalioulem6  26303  dchrptlem2  27234  lgsdchr  27324  mul2sq  27388  2sqlem5  27391  pntibnd  27562  pntlemp  27579  nosupprefixmo  27670  noinfprefixmo  27671  addsproplem2  27968  negsproplem2  28027  mulsuniflem  28147  precsexlem10  28214  zaddscl  28392  zmulscld  28395  zseo  28420  z12addscl  28475  recut  28492  readdscl  28497  remulscl  28500  cgraswap  28894  cgracom  28896  cgratr  28897  flatcgra  28898  dfcgra2  28904  acopyeu  28908  ax5seg  29013  axpasch  29016  axeuclid  29038  axcontlem4  29042  axcontlem9  29047  uhgr2edg  29283  2pthon3v  30018  pjhthmo  31379  superpos  32431  chirredi  32471  cdjreui  32509  cdj3i  32518  xrofsup  32849  archiabllem2c  33279  ccfldextdgrr  33831  ordtconnlem1  34083  dya2iocnrect  34440  txpconn  35428  cvmlift2lem10  35508  cvmlift3lem7  35521  msubco  35727  mclsppslem  35779  altopelaltxp  36172  funtransport  36227  btwnconn1lem13  36295  btwnconn1lem14  36296  segletr  36310  segleantisym  36311  funray  36336  funline  36338  tailfb  36573  mblfinlem3  37862  ismblfin  37864  itg2addnc  37877  ftc1anclem6  37901  heibor1lem  38012  crngohomfo  38209  ispridlc  38273  prter1  39161  hl2at  39687  cdlemn11pre  41492  dihord2pre  41507  dihord4  41540  dihmeetlem20N  41608  mapdpglem32  41987  diophin  43035  diophun  43036  iunrelexpuztr  43981  mullimc  45883  mullimcf  45890  addlimc  45913  fourierdlem42  46414  fourierdlem80  46451  sge0resplit  46671  hoiqssbllem3  46889