Theorem reeanv 3292

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  3reeanv  3293  2ralorOLD  3295  2reu4lem  4453  disjxiun  5067  fliftfun  7163  frrlem9  8081  tfrlem5  8182  uniinqs  8544  eroveu  8559  erovlem  8560  xpf1o  8875  unxpdomlem3  8958  unfiOLD  9011  finsschain  9056  dffi3  9120  rankxplim3  9570  xpnum  9640  kmlem9  9845  sornom  9964  fpwwe2lem11  10328  cnegex  11086  zaddcl  12290  rexanre  14986  o1lo1  15174  o1co  15223  rlimcn3  15227  o1of2  15250  lo1add  15264  lo1mul  15265  summo  15357  ntrivcvgmul  15542  prodmolem2  15573  prodmo  15574  dvds2lem  15906  odd2np1  15978  opoe  16000  omoe  16001  opeo  16002  omeo  16003  bezoutlem4  16178  gcddiv  16187  divgcdcoprmex  16299  pcqmul  16482  pcadd  16518  mul4sq  16583  4sqlem12  16585  prmgaplem7  16686  cyccom  18737  gaorber  18829  psgneu  19029  lsmsubm  19173  pj1eu  19217  efgredlem  19268  efgrelexlemb  19271  qusabl  19381  cygablOLD  19407  dprdsubg  19542  dvdsrtr  19809  unitgrp  19824  lss1d  20140  lsmspsn  20261  lspsolvlem  20319  lbsextlem2  20336  znfld  20680  cygznlem3  20689  psgnghm  20697  tgcl  22027  restbas  22217  ordtbas2  22250  uncmp  22462  txuni2  22624  txbas  22626  ptbasin  22636  txcnp  22679  txlly  22695  txnlly  22696  tx1stc  22709  tx2ndc  22710  fbasrn  22943  rnelfmlem  23011  fmfnfmlem3  23015  txflf  23065  qustgplem  23180  trust  23289  utoptop  23294  fmucndlem  23351  blin2  23490  metustto  23615  tgqioo  23869  minveclem3b  24497  pmltpc  24519  evthicc2  24529  ovolunlem2  24567  dyaddisj  24665  rolle  25059  dvcvx  25089  itgsubst  25118  plyadd  25283  plymul  25284  coeeu  25291  aalioulem6  25402  dchrptlem2  26318  lgsdchr  26408  mul2sq  26472  2sqlem5  26475  pntibnd  26646  pntlemp  26663  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  dfcgra2  27095  acopyeu  27099  ax5seg  27209  axpasch  27212  axeuclid  27234  axcontlem4  27238  axcontlem9  27243  uhgr2edg  27478  2pthon3v  28209  pjhthmo  29565  superpos  30617  chirredi  30657  cdjreui  30695  cdj3i  30704  xrofsup  30992  archiabllem2c  31351  ccfldextdgrr  31644  ordtconnlem1  31776  dya2iocnrect  32148  txpconn  33094  cvmlift2lem10  33174  cvmlift3lem7  33187  msubco  33393  mclsppslem  33445  ttrcltr  33702  poseq  33729  soseq  33730  nosupprefixmo  33830  noinfprefixmo  33831  altopelaltxp  34205  funtransport  34260  btwnconn1lem13  34328  btwnconn1lem14  34329  segletr  34343  segleantisym  34344  funray  34369  funline  34371  tailfb  34493  mblfinlem3  35743  ismblfin  35745  itg2addnc  35758  ftc1anclem6  35782  heibor1lem  35894  crngohomfo  36091  ispridlc  36155  prter1  36820  hl2at  37346  cdlemn11pre  39151  dihord2pre  39166  dihord4  39199  dihmeetlem20N  39267  mapdpglem32  39646  diophin  40510  diophun  40511  iunrelexpuztr  41216  mullimc  43047  mullimcf  43054  addlimc  43079  fourierdlem42  43580  fourierdlem80  43617  sge0resplit  43834  hoiqssbllem3  44052