Theorem reeanv 3201

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  3reeanv  3202  2reu4lem  4473  disjxiun  5089  fliftfun  7249  poseq  8091  soseq  8092  frrlem9  8227  tfrlem5  8302  uniinqs  8724  eroveu  8739  erovlem  8740  xpf1o  9056  unxpdomlem3  9147  finsschain  9249  dffi3  9321  ttrcltr  9612  rankxplim3  9777  xpnum  9847  kmlem9  10053  sornom  10171  fpwwe2lem11  10535  cnegex  11297  zaddcl  12515  rexanre  15254  o1lo1  15444  o1co  15493  rlimcn3  15497  o1of2  15520  lo1add  15534  lo1mul  15535  summo  15624  ntrivcvgmul  15809  prodmolem2  15842  prodmo  15843  dvds2lem  16179  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  bezoutlem4  16453  gcddiv  16462  divgcdcoprmex  16577  pcqmul  16765  pcadd  16801  mul4sq  16866  4sqlem12  16868  prmgaplem7  16969  cyccom  19082  gaorber  19187  psgneu  19385  lsmsubm  19532  pj1eu  19575  efgredlem  19626  efgrelexlemb  19629  qusabl  19744  dprdsubg  19905  dvdsrtr  20253  unitgrp  20268  lss1d  20866  lsmspsn  20988  lspsolvlem  21049  lbsextlem2  21066  znfld  21467  cygznlem3  21476  psgnghm  21487  tgcl  22854  restbas  23043  ordtbas2  23076  uncmp  23288  txuni2  23450  txbas  23452  ptbasin  23462  txcnp  23505  txlly  23521  txnlly  23522  tx1stc  23535  tx2ndc  23536  fbasrn  23769  rnelfmlem  23837  fmfnfmlem3  23841  txflf  23891  qustgplem  24006  trust  24115  utoptop  24120  fmucndlem  24176  blin2  24315  metustto  24439  tgqioo  24686  minveclem3b  25326  pmltpc  25349  evthicc2  25359  ovolunlem2  25397  dyaddisj  25495  rolle  25892  dvcvx  25923  itgsubst  25954  plyadd  26120  plymul  26121  coeeu  26128  aalioulem6  26243  dchrptlem2  27174  lgsdchr  27264  mul2sq  27328  2sqlem5  27331  pntibnd  27502  pntlemp  27519  nosupprefixmo  27610  noinfprefixmo  27611  addsproplem2  27882  negsproplem2  27940  mulsuniflem  28057  precsexlem10  28123  zaddscl  28287  zmulscld  28290  zseo  28314  zs12addscl  28354  recut  28365  readdscl  28368  remulscl  28371  cgraswap  28765  cgracom  28767  cgratr  28768  flatcgra  28769  dfcgra2  28775  acopyeu  28779  ax5seg  28883  axpasch  28886  axeuclid  28908  axcontlem4  28912  axcontlem9  28917  uhgr2edg  29153  2pthon3v  29888  pjhthmo  31246  superpos  32298  chirredi  32338  cdjreui  32376  cdj3i  32385  xrofsup  32711  archiabllem2c  33138  ccfldextdgrr  33645  ordtconnlem1  33897  dya2iocnrect  34255  txpconn  35215  cvmlift2lem10  35295  cvmlift3lem7  35308  msubco  35514  mclsppslem  35566  altopelaltxp  35960  funtransport  36015  btwnconn1lem13  36083  btwnconn1lem14  36084  segletr  36098  segleantisym  36099  funray  36124  funline  36126  tailfb  36361  mblfinlem3  37649  ismblfin  37651  itg2addnc  37664  ftc1anclem6  37688  heibor1lem  37799  crngohomfo  37996  ispridlc  38060  prter1  38868  hl2at  39394  cdlemn11pre  41199  dihord2pre  41214  dihord4  41247  dihmeetlem20N  41315  mapdpglem32  41694  diophin  42755  diophun  42756  iunrelexpuztr  43702  mullimc  45607  mullimcf  45614  addlimc  45639  fourierdlem42  46140  fourierdlem80  46177  sge0resplit  46397  hoiqssbllem3  46615