Theorem reeanv 3320

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∈ wcel 2111  ∃wrex 3107

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  3reeanv  3321  2ralor  3322  2reu4lem  4423  disjxiun  5027  fliftfun  7044  tfrlem5  7999  uniinqs  8360  eroveu  8375  erovlem  8376  xpf1o  8663  unxpdomlem3  8708  unfi  8769  finsschain  8815  dffi3  8879  rankxplim3  9294  xpnum  9364  kmlem9  9569  sornom  9688  fpwwe2lem12  10052  cnegex  10810  zaddcl  12010  rexanre  14698  o1lo1  14886  o1co  14935  rlimcn2  14939  o1of2  14961  lo1add  14975  lo1mul  14976  summo  15066  ntrivcvgmul  15250  prodmolem2  15281  prodmo  15282  dvds2lem  15614  odd2np1  15682  opoe  15704  omoe  15705  opeo  15706  omeo  15707  bezoutlem4  15880  gcddiv  15889  divgcdcoprmex  16000  pcqmul  16180  pcadd  16215  mul4sq  16280  4sqlem12  16282  prmgaplem7  16383  cyccom  18338  gaorber  18430  psgneu  18626  lsmsubm  18770  pj1eu  18814  efgredlem  18865  efgrelexlemb  18868  qusabl  18978  cygablOLD  19004  dprdsubg  19139  dvdsrtr  19398  unitgrp  19413  lss1d  19728  lsmspsn  19849  lspsolvlem  19907  lbsextlem2  19924  znfld  20252  cygznlem3  20261  psgnghm  20269  tgcl  21574  restbas  21763  ordtbas2  21796  uncmp  22008  txuni2  22170  txbas  22172  ptbasin  22182  txcnp  22225  txlly  22241  txnlly  22242  tx1stc  22255  tx2ndc  22256  fbasrn  22489  rnelfmlem  22557  fmfnfmlem3  22561  txflf  22611  qustgplem  22726  trust  22835  utoptop  22840  fmucndlem  22897  blin2  23036  metustto  23160  tgqioo  23405  minveclem3b  24032  pmltpc  24054  evthicc2  24064  ovolunlem2  24102  dyaddisj  24200  rolle  24593  dvcvx  24623  itgsubst  24652  plyadd  24814  plymul  24815  coeeu  24822  aalioulem6  24933  dchrptlem2  25849  lgsdchr  25939  mul2sq  26003  2sqlem5  26006  pntibnd  26177  pntlemp  26194  cgraswap  26614  cgracom  26616  cgratr  26617  flatcgra  26618  dfcgra2  26624  acopyeu  26628  ax5seg  26732  axpasch  26735  axeuclid  26757  axcontlem4  26761  axcontlem9  26766  uhgr2edg  26998  2pthon3v  27729  pjhthmo  29085  superpos  30137  chirredi  30177  cdjreui  30215  cdj3i  30224  xrofsup  30518  archiabllem2c  30874  ccfldextdgrr  31145  ordtconnlem1  31277  dya2iocnrect  31649  txpconn  32592  cvmlift2lem10  32672  cvmlift3lem7  32685  msubco  32891  mclsppslem  32943  poseq  33208  soseq  33209  frrlem9  33244  noprefixmo  33315  altopelaltxp  33550  funtransport  33605  btwnconn1lem13  33673  btwnconn1lem14  33674  segletr  33688  segleantisym  33689  funray  33714  funline  33716  tailfb  33838  mblfinlem3  35096  ismblfin  35098  itg2addnc  35111  ftc1anclem6  35135  heibor1lem  35247  crngohomfo  35444  ispridlc  35508  prter1  36175  hl2at  36701  cdlemn11pre  38506  dihord2pre  38521  dihord4  38554  dihmeetlem20N  38622  mapdpglem32  39001  diophin  39713  diophun  39714  iunrelexpuztr  40420  mullimc  42258  mullimcf  42265  addlimc  42290  fourierdlem42  42791  fourierdlem80  42828  sge0resplit  43045  hoiqssbllem3  43263