Theorem reeanv 3285

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

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

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 3075  df-rex 3076

This theorem is referenced by:  3reeanv  3286  2ralor  3287  2reu4lem  4421  disjxiun  5033  fliftfun  7065  tfrlem5  8032  uniinqs  8393  eroveu  8408  erovlem  8409  xpf1o  8714  unxpdomlem3  8775  unfiOLD  8831  finsschain  8877  dffi3  8941  rankxplim3  9356  xpnum  9426  kmlem9  9631  sornom  9750  fpwwe2lem11  10114  cnegex  10872  zaddcl  12074  rexanre  14767  o1lo1  14955  o1co  15004  rlimcn2  15008  o1of2  15030  lo1add  15044  lo1mul  15045  summo  15135  ntrivcvgmul  15319  prodmolem2  15350  prodmo  15351  dvds2lem  15683  odd2np1  15755  opoe  15777  omoe  15778  opeo  15779  omeo  15780  bezoutlem4  15954  gcddiv  15963  divgcdcoprmex  16075  pcqmul  16258  pcadd  16293  mul4sq  16358  4sqlem12  16360  prmgaplem7  16461  cyccom  18426  gaorber  18518  psgneu  18714  lsmsubm  18858  pj1eu  18902  efgredlem  18953  efgrelexlemb  18956  qusabl  19066  cygablOLD  19092  dprdsubg  19227  dvdsrtr  19486  unitgrp  19501  lss1d  19816  lsmspsn  19937  lspsolvlem  19995  lbsextlem2  20012  znfld  20341  cygznlem3  20350  psgnghm  20358  tgcl  21682  restbas  21871  ordtbas2  21904  uncmp  22116  txuni2  22278  txbas  22280  ptbasin  22290  txcnp  22333  txlly  22349  txnlly  22350  tx1stc  22363  tx2ndc  22364  fbasrn  22597  rnelfmlem  22665  fmfnfmlem3  22669  txflf  22719  qustgplem  22834  trust  22943  utoptop  22948  fmucndlem  23005  blin2  23144  metustto  23268  tgqioo  23514  minveclem3b  24141  pmltpc  24163  evthicc2  24173  ovolunlem2  24211  dyaddisj  24309  rolle  24702  dvcvx  24732  itgsubst  24761  plyadd  24926  plymul  24927  coeeu  24934  aalioulem6  25045  dchrptlem2  25961  lgsdchr  26051  mul2sq  26115  2sqlem5  26118  pntibnd  26289  pntlemp  26306  cgraswap  26726  cgracom  26728  cgratr  26729  flatcgra  26730  dfcgra2  26736  acopyeu  26740  ax5seg  26844  axpasch  26847  axeuclid  26869  axcontlem4  26873  axcontlem9  26878  uhgr2edg  27110  2pthon3v  27841  pjhthmo  29197  superpos  30249  chirredi  30289  cdjreui  30327  cdj3i  30336  xrofsup  30626  archiabllem2c  30987  ccfldextdgrr  31275  ordtconnlem1  31407  dya2iocnrect  31779  txpconn  32722  cvmlift2lem10  32802  cvmlift3lem7  32815  msubco  33021  mclsppslem  33073  poseq  33369  soseq  33370  frrlem9  33405  nosupprefixmo  33500  noinfprefixmo  33501  altopelaltxp  33861  funtransport  33916  btwnconn1lem13  33984  btwnconn1lem14  33985  segletr  33999  segleantisym  34000  funray  34025  funline  34027  tailfb  34149  mblfinlem3  35410  ismblfin  35412  itg2addnc  35425  ftc1anclem6  35449  heibor1lem  35561  crngohomfo  35758  ispridlc  35822  prter1  36489  hl2at  37015  cdlemn11pre  38820  dihord2pre  38835  dihord4  38868  dihmeetlem20N  38936  mapdpglem32  39315  diophin  40121  diophun  40122  iunrelexpuztr  40828  mullimc  42659  mullimcf  42666  addlimc  42691  fourierdlem42  43192  fourierdlem80  43229  sge0resplit  43446  hoiqssbllem3  43664