Theorem reeanv 3209

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

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 1912

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

This theorem is referenced by:  3reeanv  3210  2reu4lem  4463  disjxiun  5082  fliftfun  7267  poseq  8108  soseq  8109  frrlem9  8244  tfrlem5  8319  uniinqs  8744  eroveu  8759  erovlem  8760  xpf1o  9077  unxpdomlem3  9168  finsschain  9269  dffi3  9344  ttrcltr  9637  rankxplim3  9805  xpnum  9875  kmlem9  10081  sornom  10199  fpwwe2lem11  10564  cnegex  11327  zaddcl  12567  rexanre  15309  o1lo1  15499  o1co  15548  rlimcn3  15552  o1of2  15575  lo1add  15589  lo1mul  15590  summo  15679  ntrivcvgmul  15867  prodmolem2  15900  prodmo  15901  dvds2lem  16237  odd2np1  16310  opoe  16332  omoe  16333  opeo  16334  omeo  16335  bezoutlem4  16511  gcddiv  16520  divgcdcoprmex  16635  pcqmul  16824  pcadd  16860  mul4sq  16925  4sqlem12  16927  prmgaplem7  17028  cyccom  19178  gaorber  19283  psgneu  19481  lsmsubm  19628  pj1eu  19671  efgredlem  19722  efgrelexlemb  19725  qusabl  19840  dprdsubg  20001  dvdsrtr  20348  unitgrp  20363  lss1d  20958  lsmspsn  21079  lspsolvlem  21140  lbsextlem2  21157  znfld  21540  cygznlem3  21549  psgnghm  21560  tgcl  22934  restbas  23123  ordtbas2  23156  uncmp  23368  txuni2  23530  txbas  23532  ptbasin  23542  txcnp  23585  txlly  23601  txnlly  23602  tx1stc  23615  tx2ndc  23616  fbasrn  23849  rnelfmlem  23917  fmfnfmlem3  23921  txflf  23971  qustgplem  24086  trust  24194  utoptop  24199  fmucndlem  24255  blin2  24394  metustto  24518  tgqioo  24765  minveclem3b  25395  pmltpc  25417  evthicc2  25427  ovolunlem2  25465  dyaddisj  25563  rolle  25957  dvcvx  25987  itgsubst  26016  plyadd  26182  plymul  26183  coeeu  26190  aalioulem6  26303  dchrptlem2  27228  lgsdchr  27318  mul2sq  27382  2sqlem5  27385  pntibnd  27556  pntlemp  27573  nosupprefixmo  27664  noinfprefixmo  27665  addsproplem2  27962  negsproplem2  28021  mulsuniflem  28141  precsexlem10  28208  zaddscl  28386  zmulscld  28389  zseo  28414  z12addscl  28469  recut  28486  readdscl  28491  remulscl  28494  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  dfcgra2  28898  acopyeu  28902  ax5seg  29007  axpasch  29010  axeuclid  29032  axcontlem4  29036  axcontlem9  29041  uhgr2edg  29277  2pthon3v  30011  pjhthmo  31373  superpos  32425  chirredi  32465  cdjreui  32503  cdj3i  32512  xrofsup  32840  archiabllem2c  33256  ccfldextdgrr  33816  ordtconnlem1  34068  dya2iocnrect  34425  txpconn  35414  cvmlift2lem10  35494  cvmlift3lem7  35507  msubco  35713  mclsppslem  35765  altopelaltxp  36158  funtransport  36213  btwnconn1lem13  36281  btwnconn1lem14  36282  segletr  36296  segleantisym  36297  funray  36322  funline  36324  tailfb  36559  mblfinlem3  37980  ismblfin  37982  itg2addnc  37995  ftc1anclem6  38019  heibor1lem  38130  crngohomfo  38327  ispridlc  38391  prter1  39325  hl2at  39851  cdlemn11pre  41656  dihord2pre  41671  dihord4  41704  dihmeetlem20N  41772  mapdpglem32  42151  diophin  43204  diophun  43205  iunrelexpuztr  44146  mullimc  46046  mullimcf  46053  addlimc  46076  fourierdlem42  46577  fourierdlem80  46614  sge0resplit  46834  hoiqssbllem3  47052