Theorem reeanv 3206

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3050  df-rex 3059

This theorem is referenced by:  3reeanv  3207  2reu4lem  4474  disjxiun  5093  fliftfun  7256  poseq  8098  soseq  8099  frrlem9  8234  tfrlem5  8309  uniinqs  8732  eroveu  8747  erovlem  8748  xpf1o  9065  unxpdomlem3  9156  finsschain  9257  dffi3  9332  ttrcltr  9623  rankxplim3  9791  xpnum  9861  kmlem9  10067  sornom  10185  fpwwe2lem11  10550  cnegex  11312  zaddcl  12529  rexanre  15268  o1lo1  15458  o1co  15507  rlimcn3  15511  o1of2  15534  lo1add  15548  lo1mul  15549  summo  15638  ntrivcvgmul  15823  prodmolem2  15856  prodmo  15857  dvds2lem  16193  odd2np1  16266  opoe  16288  omoe  16289  opeo  16290  omeo  16291  bezoutlem4  16467  gcddiv  16476  divgcdcoprmex  16591  pcqmul  16779  pcadd  16815  mul4sq  16880  4sqlem12  16882  prmgaplem7  16983  cyccom  19130  gaorber  19235  psgneu  19433  lsmsubm  19580  pj1eu  19623  efgredlem  19674  efgrelexlemb  19677  qusabl  19792  dprdsubg  19953  dvdsrtr  20302  unitgrp  20317  lss1d  20912  lsmspsn  21034  lspsolvlem  21095  lbsextlem2  21112  znfld  21513  cygznlem3  21522  psgnghm  21533  tgcl  22911  restbas  23100  ordtbas2  23133  uncmp  23345  txuni2  23507  txbas  23509  ptbasin  23519  txcnp  23562  txlly  23578  txnlly  23579  tx1stc  23592  tx2ndc  23593  fbasrn  23826  rnelfmlem  23894  fmfnfmlem3  23898  txflf  23948  qustgplem  24063  trust  24171  utoptop  24176  fmucndlem  24232  blin2  24371  metustto  24495  tgqioo  24742  minveclem3b  25382  pmltpc  25405  evthicc2  25415  ovolunlem2  25453  dyaddisj  25551  rolle  25948  dvcvx  25979  itgsubst  26010  plyadd  26176  plymul  26177  coeeu  26184  aalioulem6  26299  dchrptlem2  27230  lgsdchr  27320  mul2sq  27384  2sqlem5  27387  pntibnd  27558  pntlemp  27575  nosupprefixmo  27666  noinfprefixmo  27667  addsproplem2  27940  negsproplem2  27998  mulsuniflem  28118  precsexlem10  28184  zaddscl  28352  zmulscld  28355  zseo  28380  zs12addscl  28426  recut  28439  readdscl  28444  remulscl  28447  cgraswap  28841  cgracom  28843  cgratr  28844  flatcgra  28845  dfcgra2  28851  acopyeu  28855  ax5seg  28960  axpasch  28963  axeuclid  28985  axcontlem4  28989  axcontlem9  28994  uhgr2edg  29230  2pthon3v  29965  pjhthmo  31326  superpos  32378  chirredi  32418  cdjreui  32456  cdj3i  32465  xrofsup  32796  archiabllem2c  33226  ccfldextdgrr  33778  ordtconnlem1  34030  dya2iocnrect  34387  txpconn  35375  cvmlift2lem10  35455  cvmlift3lem7  35468  msubco  35674  mclsppslem  35726  altopelaltxp  36119  funtransport  36174  btwnconn1lem13  36242  btwnconn1lem14  36243  segletr  36257  segleantisym  36258  funray  36283  funline  36285  tailfb  36520  mblfinlem3  37799  ismblfin  37801  itg2addnc  37814  ftc1anclem6  37838  heibor1lem  37949  crngohomfo  38146  ispridlc  38210  prter1  39078  hl2at  39604  cdlemn11pre  41409  dihord2pre  41424  dihord4  41457  dihmeetlem20N  41525  mapdpglem32  41904  diophin  42956  diophun  42957  iunrelexpuztr  43902  mullimc  45804  mullimcf  45811  addlimc  45834  fourierdlem42  46335  fourierdlem80  46372  sge0resplit  46592  hoiqssbllem3  46810