Theorem reeanv 3235

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∈ wcel 2143  ∃wrex 3087

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-ral 3078  df-rex 3088

This theorem is referenced by:  3reeanv  3236  2reu4lem  4478  disjxiun  5098  fliftfun  7297  poseq  8139  soseq  8140  frrlem9  8276  tfrlem5  8351  uniinqs  8780  eroveu  8795  erovlem  8796  xpf1o  9112  unxpdomlem3  9203  finsschain  9303  dffi3  9378  ttrcltr  9672  rankxplim3  9840  xpnum  9910  kmlem9  10116  sornom  10235  fpwwe2lem11  10600  cnegex  11365  zaddcl  12612  rexanre  15375  o1lo1  15565  o1co  15614  rlimcn3  15618  o1of2  15641  lo1add  15655  lo1mul  15656  summo  15745  ntrivcvgmul  15933  prodmolem2  15966  prodmo  15967  dvds2lem  16303  odd2np1  16376  opoe  16398  omoe  16399  opeo  16400  omeo  16401  bezoutlem4  16577  gcddiv  16586  divgcdcoprmex  16701  pcqmul  16890  pcadd  16926  mul4sq  16991  4sqlem12  16993  prmgaplem7  17094  cyccom  19245  gaorber  19349  psgneu  19547  lsmsubm  19694  pj1eu  19737  efgredlem  19788  efgrelexlemb  19791  qusabl  19906  dprdsubg  20067  dvdsrtr  20418  unitgrp  20433  lss1d  21031  lsmspsn  21152  lspsolvlem  21213  lbsextlem2  21230  znfld  21613  cygznlem3  21622  psgnghm  21633  tgcl  23030  restbas  23219  ordtbas2  23252  uncmp  23464  txuni2  23626  txbas  23628  ptbasin  23638  txcnp  23681  txlly  23697  txnlly  23698  tx1stc  23711  tx2ndc  23712  fbasrn  23945  rnelfmlem  24013  fmfnfmlem3  24017  txflf  24067  qustgplem  24182  trust  24290  utoptop  24295  fmucndlem  24351  blin2  24490  metustto  24614  tgqioo  24861  minveclem3b  25491  pmltpc  25513  evthicc2  25523  ovolunlem2  25561  dyaddisj  25659  rolle  26053  dvcvx  26083  itgsubst  26112  plyadd  26278  plymul  26279  coeeu  26286  aalioulem6  26402  dchrptlem2  27330  lgsdchr  27420  mul2sq  27484  2sqlem5  27487  pntibnd  27658  pntlemp  27675  nosupprefixmo  27765  noinfprefixmo  27766  addsproplem2  28064  negsproplem2  28123  mulsuniflem  28243  precsexlem10  28310  zaddscl  28488  zmulscld  28491  zseo  28516  z12addscl  28571  recut  28588  readdscl  28593  remulscl  28596  cgraswap  29015  cgracom  29017  cgratr  29018  flatcgra  29019  dfcgra2  29025  acopyeu  29029  ax5seg  29140  axpasch  29143  axeuclid  29165  axcontlem4  29169  axcontlem9  29174  uhgr2edg  29410  2pthon3v  30144  pjhthmo  31506  superpos  32558  chirredi  32598  cdjreui  32636  cdj3i  32645  xrofsup  32970  archiabllem2c  33376  ccfldextdgrr  33970  ordtconnlem1  34222  dya2iocnrect  34579  txpconn  35583  cvmlift2lem10  35663  cvmlift3lem7  35676  msubco  35882  mclsppslem  35934  altopelaltxp  36327  funtransport  36382  btwnconn1lem13  36450  btwnconn1lem14  36451  segletr  36465  segleantisym  36466  funray  36491  funline  36493  tailfb  36738  mblfinlem3  38159  ismblfin  38161  itg2addnc  38174  ftc1anclem6  38198  heibor1lem  38309  crngohomfo  38506  ispridlc  38570  prter1  39504  hl2at  40030  cdlemn11pre  41835  dihord2pre  41850  dihord4  41883  dihmeetlem20N  41951  mapdpglem32  42330  diophin  43354  diophun  43355  iunrelexpuztr  44296  mullimc  46193  mullimcf  46200  addlimc  46223  fourierdlem42  46724  fourierdlem80  46761  sge0resplit  46981  hoiqssbllem3  47199