Theorem reeanv 3204

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3048  df-rex 3057

This theorem is referenced by:  3reeanv  3205  2reu4lem  4469  disjxiun  5086  fliftfun  7246  poseq  8088  soseq  8089  frrlem9  8224  tfrlem5  8299  uniinqs  8721  eroveu  8736  erovlem  8737  xpf1o  9052  unxpdomlem3  9142  finsschain  9243  dffi3  9315  ttrcltr  9606  rankxplim3  9774  xpnum  9844  kmlem9  10050  sornom  10168  fpwwe2lem11  10532  cnegex  11294  zaddcl  12512  rexanre  15254  o1lo1  15444  o1co  15493  rlimcn3  15497  o1of2  15520  lo1add  15534  lo1mul  15535  summo  15624  ntrivcvgmul  15809  prodmolem2  15842  prodmo  15843  dvds2lem  16179  odd2np1  16252  opoe  16274  omoe  16275  opeo  16276  omeo  16277  bezoutlem4  16453  gcddiv  16462  divgcdcoprmex  16577  pcqmul  16765  pcadd  16801  mul4sq  16866  4sqlem12  16868  prmgaplem7  16969  cyccom  19115  gaorber  19220  psgneu  19418  lsmsubm  19565  pj1eu  19608  efgredlem  19659  efgrelexlemb  19662  qusabl  19777  dprdsubg  19938  dvdsrtr  20286  unitgrp  20301  lss1d  20896  lsmspsn  21018  lspsolvlem  21079  lbsextlem2  21096  znfld  21497  cygznlem3  21506  psgnghm  21517  tgcl  22884  restbas  23073  ordtbas2  23106  uncmp  23318  txuni2  23480  txbas  23482  ptbasin  23492  txcnp  23535  txlly  23551  txnlly  23552  tx1stc  23565  tx2ndc  23566  fbasrn  23799  rnelfmlem  23867  fmfnfmlem3  23871  txflf  23921  qustgplem  24036  trust  24144  utoptop  24149  fmucndlem  24205  blin2  24344  metustto  24468  tgqioo  24715  minveclem3b  25355  pmltpc  25378  evthicc2  25388  ovolunlem2  25426  dyaddisj  25524  rolle  25921  dvcvx  25952  itgsubst  25983  plyadd  26149  plymul  26150  coeeu  26157  aalioulem6  26272  dchrptlem2  27203  lgsdchr  27293  mul2sq  27357  2sqlem5  27360  pntibnd  27531  pntlemp  27548  nosupprefixmo  27639  noinfprefixmo  27640  addsproplem2  27913  negsproplem2  27971  mulsuniflem  28088  precsexlem10  28154  zaddscl  28318  zmulscld  28321  zseo  28345  zs12addscl  28387  recut  28398  readdscl  28401  remulscl  28404  cgraswap  28798  cgracom  28800  cgratr  28801  flatcgra  28802  dfcgra2  28808  acopyeu  28812  ax5seg  28916  axpasch  28919  axeuclid  28941  axcontlem4  28945  axcontlem9  28950  uhgr2edg  29186  2pthon3v  29921  pjhthmo  31282  superpos  32334  chirredi  32374  cdjreui  32412  cdj3i  32421  xrofsup  32750  archiabllem2c  33164  ccfldextdgrr  33685  ordtconnlem1  33937  dya2iocnrect  34294  txpconn  35276  cvmlift2lem10  35356  cvmlift3lem7  35369  msubco  35575  mclsppslem  35627  altopelaltxp  36020  funtransport  36075  btwnconn1lem13  36143  btwnconn1lem14  36144  segletr  36158  segleantisym  36159  funray  36184  funline  36186  tailfb  36421  mblfinlem3  37709  ismblfin  37711  itg2addnc  37724  ftc1anclem6  37748  heibor1lem  37859  crngohomfo  38056  ispridlc  38120  prter1  38988  hl2at  39514  cdlemn11pre  41319  dihord2pre  41334  dihord4  41367  dihmeetlem20N  41435  mapdpglem32  41814  diophin  42875  diophun  42876  iunrelexpuztr  43822  mullimc  45726  mullimcf  45733  addlimc  45756  fourierdlem42  46257  fourierdlem80  46294  sge0resplit  46514  hoiqssbllem3  46732