Theorem reeanv 3240

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2146  ∃wrex 3092

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3083  df-rex 3093

This theorem is used by:  3reeanv  3241  2reu4lem  4487  disjxiun  5109  fliftfun  7314  poseq  8156  soseq  8157  frrlem9  8293  tfrlem5  8368  uniinqs  8797  eroveu  8812  erovlem  8813  xpf1o  9129  unxpdomlem3  9220  finsschain  9318  dffi3  9393  ttrcltr  9687  rankxplim3  9855  xpnum  9948  kmlem9  10153  sornom  10271  fpwwe2lem11  10636  cnegex  11401  zaddcl  12644  rexanre  15409  o1lo1  15599  o1co  15648  rlimcn3  15652  o1of2  15675  lo1add  15689  lo1mul  15690  summo  15779  ntrivcvgmul  15967  prodmolem2  16000  prodmo  16001  dvds2lem  16336  odd2np1  16409  opoe  16431  omoe  16432  opeo  16433  omeo  16434  bezoutlem4  16610  gcddiv  16619  divgcdcoprmex  16734  pcqmul  16923  pcadd  16959  mul4sq  17024  4sqlem12  17026  prmgaplem7  17127  cyccom  19284  gaorber  19388  psgneu  19586  lsmsubm  19733  pj1eu  19776  efgredlem  19827  efgrelexlemb  19830  qusabl  19945  dprdsubg  20106  dvdsrtr  20461  unitgrp  20476  crngrhmfo  20589  lss1d  21099  lsmspsn  21220  lspsolvlem  21281  lbsextlem2  21298  znfld  21725  cygznlem3  21734  psgnghm  21745  tgcl  23141  restbas  23330  ordtbas2  23363  uncmp  23575  txuni2  23737  txbas  23739  ptbasin  23749  txcnp  23792  txlly  23808  txnlly  23809  tx1stc  23822  tx2ndc  23823  fbasrn  24056  rnelfmlem  24124  fmfnfmlem3  24128  txflf  24178  qustgplem  24293  trust  24401  utoptop  24406  fmucndlem  24462  blin2  24601  metustto  24725  tgqioo  24972  minveclem3b  25602  pmltpc  25624  evthicc2  25634  ovolunlem2  25672  dyaddisj  25770  rolle  26164  dvcvx  26194  itgsubst  26223  plyadd  26389  plymul  26390  coeeu  26397  aalioulem6  26515  dchrptlem2  27444  lgsdchr  27534  mul2sq  27598  2sqlem5  27601  pntibnd  27772  pntlemp  27789  nosupprefixmo  27879  noinfprefixmo  27880  addsproplem2  28178  negsproplem2  28237  mulsuniflem  28357  precsexlem10  28424  zaddscl  28602  zmulscld  28605  zseo  28630  z12addscl  28685  recut  28702  readdscl  28707  remulscl  28710  cgraswap  29146  cgracom  29148  cgratr  29149  flatcgra  29150  dfcgra2  29156  acopyeu  29160  ax5seg  29303  axpasch  29306  axeuclid  29328  axcontlem4  29332  axcontlem9  29337  uhgr2edg  29573  2pthon3v  30307  pjhthmo  31669  superpos  32721  chirredi  32761  cdjreui  32799  cdj3i  32808  xrofsup  33127  archiabllem2c  33528  ccfldextdgrr  34075  ordtconnlem1  34327  dya2iocnrect  34684  txpconn  35736  cvmlift2lem10  35816  cvmlift3lem7  35829  msubco  36035  mclsppslem  36087  altopelaltxp  36480  funtransport  36535  btwnconn1lem13  36603  btwnconn1lem14  36604  segletr  36618  segleantisym  36619  funray  36644  funline  36646  tailfb  36920  mblfinlem3  38342  ismblfin  38344  itg2addnc  38357  ftc1anclem6  38381  heibor1lem  38492  crngohomfo  38689  ispridlc  38753  prter1  39685  hl2at  40211  cdlemn11pre  42016  dihord2pre  42031  dihord4  42064  dihmeetlem20N  42132  mapdpglem32  42511  diophin  43535  diophun  43536  iunrelexpuztr  44477  mullimc  46364  mullimcf  46371  addlimc  46394  fourierdlem42  46895  fourierdlem80  46932  sge0resplit  47152  hoiqssbllem3  47370