Theorem reeanv 3210

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

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

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 3046  df-rex 3055

This theorem is referenced by:  3reeanv  3211  2reu4lem  4488  disjxiun  5107  fliftfun  7290  poseq  8140  soseq  8141  frrlem9  8276  tfrlem5  8351  uniinqs  8773  eroveu  8788  erovlem  8789  xpf1o  9109  unxpdomlem3  9206  finsschain  9317  dffi3  9389  ttrcltr  9676  rankxplim3  9841  xpnum  9911  kmlem9  10119  sornom  10237  fpwwe2lem11  10601  cnegex  11362  zaddcl  12580  rexanre  15320  o1lo1  15510  o1co  15559  rlimcn3  15563  o1of2  15586  lo1add  15600  lo1mul  15601  summo  15690  ntrivcvgmul  15875  prodmolem2  15908  prodmo  15909  dvds2lem  16245  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  bezoutlem4  16519  gcddiv  16528  divgcdcoprmex  16643  pcqmul  16831  pcadd  16867  mul4sq  16932  4sqlem12  16934  prmgaplem7  17035  cyccom  19142  gaorber  19247  psgneu  19443  lsmsubm  19590  pj1eu  19633  efgredlem  19684  efgrelexlemb  19687  qusabl  19802  dprdsubg  19963  dvdsrtr  20284  unitgrp  20299  lss1d  20876  lsmspsn  20998  lspsolvlem  21059  lbsextlem2  21076  znfld  21477  cygznlem3  21486  psgnghm  21496  tgcl  22863  restbas  23052  ordtbas2  23085  uncmp  23297  txuni2  23459  txbas  23461  ptbasin  23471  txcnp  23514  txlly  23530  txnlly  23531  tx1stc  23544  tx2ndc  23545  fbasrn  23778  rnelfmlem  23846  fmfnfmlem3  23850  txflf  23900  qustgplem  24015  trust  24124  utoptop  24129  fmucndlem  24185  blin2  24324  metustto  24448  tgqioo  24695  minveclem3b  25335  pmltpc  25358  evthicc2  25368  ovolunlem2  25406  dyaddisj  25504  rolle  25901  dvcvx  25932  itgsubst  25963  plyadd  26129  plymul  26130  coeeu  26137  aalioulem6  26252  dchrptlem2  27183  lgsdchr  27273  mul2sq  27337  2sqlem5  27340  pntibnd  27511  pntlemp  27528  nosupprefixmo  27619  noinfprefixmo  27620  addsproplem2  27884  negsproplem2  27942  mulsuniflem  28059  precsexlem10  28125  zaddscl  28289  zmulscld  28292  zseo  28315  recut  28354  readdscl  28357  remulscl  28360  cgraswap  28754  cgracom  28756  cgratr  28757  flatcgra  28758  dfcgra2  28764  acopyeu  28768  ax5seg  28872  axpasch  28875  axeuclid  28897  axcontlem4  28901  axcontlem9  28906  uhgr2edg  29142  2pthon3v  29880  pjhthmo  31238  superpos  32290  chirredi  32330  cdjreui  32368  cdj3i  32377  xrofsup  32697  archiabllem2c  33156  ccfldextdgrr  33674  ordtconnlem1  33921  dya2iocnrect  34279  txpconn  35226  cvmlift2lem10  35306  cvmlift3lem7  35319  msubco  35525  mclsppslem  35577  altopelaltxp  35971  funtransport  36026  btwnconn1lem13  36094  btwnconn1lem14  36095  segletr  36109  segleantisym  36110  funray  36135  funline  36137  tailfb  36372  mblfinlem3  37660  ismblfin  37662  itg2addnc  37675  ftc1anclem6  37699  heibor1lem  37810  crngohomfo  38007  ispridlc  38071  prter1  38879  hl2at  39406  cdlemn11pre  41211  dihord2pre  41226  dihord4  41259  dihmeetlem20N  41327  mapdpglem32  41706  diophin  42767  diophun  42768  iunrelexpuztr  43715  mullimc  45621  mullimcf  45628  addlimc  45653  fourierdlem42  46154  fourierdlem80  46191  sge0resplit  46411  hoiqssbllem3  46629