Theorem reeanv 3227

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  3reeanv  3228  2ralorOLD  3230  2reu4lem  4526  disjxiun  5146  fliftfun  7309  poseq  8144  soseq  8145  frrlem9  8279  tfrlem5  8380  uniinqs  8791  eroveu  8806  erovlem  8807  xpf1o  9139  unxpdomlem3  9252  unfiOLD  9313  finsschain  9359  dffi3  9426  ttrcltr  9711  rankxplim3  9876  xpnum  9946  kmlem9  10153  sornom  10272  fpwwe2lem11  10636  cnegex  11395  zaddcl  12602  rexanre  15293  o1lo1  15481  o1co  15530  rlimcn3  15534  o1of2  15557  lo1add  15571  lo1mul  15572  summo  15663  ntrivcvgmul  15848  prodmolem2  15879  prodmo  15880  dvds2lem  16212  odd2np1  16284  opoe  16306  omoe  16307  opeo  16308  omeo  16309  bezoutlem4  16484  gcddiv  16493  divgcdcoprmex  16603  pcqmul  16786  pcadd  16822  mul4sq  16887  4sqlem12  16889  prmgaplem7  16990  cyccom  19080  gaorber  19172  psgneu  19374  lsmsubm  19521  pj1eu  19564  efgredlem  19615  efgrelexlemb  19618  qusabl  19733  dprdsubg  19894  dvdsrtr  20182  unitgrp  20197  lss1d  20574  lsmspsn  20695  lspsolvlem  20755  lbsextlem2  20772  znfld  21116  cygznlem3  21125  psgnghm  21133  tgcl  22472  restbas  22662  ordtbas2  22695  uncmp  22907  txuni2  23069  txbas  23071  ptbasin  23081  txcnp  23124  txlly  23140  txnlly  23141  tx1stc  23154  tx2ndc  23155  fbasrn  23388  rnelfmlem  23456  fmfnfmlem3  23460  txflf  23510  qustgplem  23625  trust  23734  utoptop  23739  fmucndlem  23796  blin2  23935  metustto  24062  tgqioo  24316  minveclem3b  24945  pmltpc  24967  evthicc2  24977  ovolunlem2  25015  dyaddisj  25113  rolle  25507  dvcvx  25537  itgsubst  25566  plyadd  25731  plymul  25732  coeeu  25739  aalioulem6  25850  dchrptlem2  26768  lgsdchr  26858  mul2sq  26922  2sqlem5  26925  pntibnd  27096  pntlemp  27113  nosupprefixmo  27203  noinfprefixmo  27204  addsproplem2  27454  negsproplem2  27503  mulsuniflem  27604  precsexlem10  27662  cgraswap  28071  cgracom  28073  cgratr  28074  flatcgra  28075  dfcgra2  28081  acopyeu  28085  ax5seg  28196  axpasch  28199  axeuclid  28221  axcontlem4  28225  axcontlem9  28230  uhgr2edg  28465  2pthon3v  29197  pjhthmo  30555  superpos  31607  chirredi  31647  cdjreui  31685  cdj3i  31694  xrofsup  31980  archiabllem2c  32341  ccfldextdgrr  32746  ordtconnlem1  32904  dya2iocnrect  33280  txpconn  34223  cvmlift2lem10  34303  cvmlift3lem7  34316  msubco  34522  mclsppslem  34574  altopelaltxp  34948  funtransport  35003  btwnconn1lem13  35071  btwnconn1lem14  35072  segletr  35086  segleantisym  35087  funray  35112  funline  35114  tailfb  35262  mblfinlem3  36527  ismblfin  36529  itg2addnc  36542  ftc1anclem6  36566  heibor1lem  36677  crngohomfo  36874  ispridlc  36938  prter1  37749  hl2at  38276  cdlemn11pre  40081  dihord2pre  40096  dihord4  40129  dihmeetlem20N  40197  mapdpglem32  40576  diophin  41510  diophun  41511  iunrelexpuztr  42470  mullimc  44332  mullimcf  44339  addlimc  44364  fourierdlem42  44865  fourierdlem80  44902  sge0resplit  45122  hoiqssbllem3  45340