Theorem reeanv 3225

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∈ wcel 2105  ∃wrex 3069

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 1912

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-ral 3061  df-rex 3070

This theorem is referenced by:  3reeanv  3226  2ralorOLD  3228  2reu4lem  4525  disjxiun  5145  fliftfun  7312  poseq  8149  soseq  8150  frrlem9  8285  tfrlem5  8386  uniinqs  8797  eroveu  8812  erovlem  8813  xpf1o  9145  unxpdomlem3  9258  unfiOLD  9319  finsschain  9365  dffi3  9432  ttrcltr  9717  rankxplim3  9882  xpnum  9952  kmlem9  10159  sornom  10278  fpwwe2lem11  10642  cnegex  11402  zaddcl  12609  rexanre  15300  o1lo1  15488  o1co  15537  rlimcn3  15541  o1of2  15564  lo1add  15578  lo1mul  15579  summo  15670  ntrivcvgmul  15855  prodmolem2  15886  prodmo  15887  dvds2lem  16219  odd2np1  16291  opoe  16313  omoe  16314  opeo  16315  omeo  16316  bezoutlem4  16491  gcddiv  16500  divgcdcoprmex  16610  pcqmul  16793  pcadd  16829  mul4sq  16894  4sqlem12  16896  prmgaplem7  16997  cyccom  19125  gaorber  19220  psgneu  19422  lsmsubm  19569  pj1eu  19612  efgredlem  19663  efgrelexlemb  19666  qusabl  19781  dprdsubg  19942  dvdsrtr  20266  unitgrp  20281  lss1d  20806  lsmspsn  20927  lspsolvlem  20988  lbsextlem2  21005  znfld  21425  cygznlem3  21434  psgnghm  21442  tgcl  22791  restbas  22981  ordtbas2  23014  uncmp  23226  txuni2  23388  txbas  23390  ptbasin  23400  txcnp  23443  txlly  23459  txnlly  23460  tx1stc  23473  tx2ndc  23474  fbasrn  23707  rnelfmlem  23775  fmfnfmlem3  23779  txflf  23829  qustgplem  23944  trust  24053  utoptop  24058  fmucndlem  24115  blin2  24254  metustto  24381  tgqioo  24635  minveclem3b  25275  pmltpc  25298  evthicc2  25308  ovolunlem2  25346  dyaddisj  25444  rolle  25841  dvcvx  25872  itgsubst  25903  plyadd  26068  plymul  26069  coeeu  26076  aalioulem6  26188  dchrptlem2  27110  lgsdchr  27200  mul2sq  27264  2sqlem5  27267  pntibnd  27438  pntlemp  27455  nosupprefixmo  27545  noinfprefixmo  27546  addsproplem2  27799  negsproplem2  27853  mulsuniflem  27961  precsexlem10  28026  recut  28103  readdscl  28106  remulscl  28109  cgraswap  28503  cgracom  28505  cgratr  28506  flatcgra  28507  dfcgra2  28513  acopyeu  28517  ax5seg  28628  axpasch  28631  axeuclid  28653  axcontlem4  28657  axcontlem9  28662  uhgr2edg  28897  2pthon3v  29629  pjhthmo  30987  superpos  32039  chirredi  32079  cdjreui  32117  cdj3i  32126  xrofsup  32412  archiabllem2c  32776  ccfldextdgrr  33200  ordtconnlem1  33367  dya2iocnrect  33743  txpconn  34686  cvmlift2lem10  34766  cvmlift3lem7  34779  msubco  34985  mclsppslem  35037  altopelaltxp  35417  funtransport  35472  btwnconn1lem13  35540  btwnconn1lem14  35541  segletr  35555  segleantisym  35556  funray  35581  funline  35583  tailfb  35725  mblfinlem3  36990  ismblfin  36992  itg2addnc  37005  ftc1anclem6  37029  heibor1lem  37140  crngohomfo  37337  ispridlc  37401  prter1  38212  hl2at  38739  cdlemn11pre  40544  dihord2pre  40559  dihord4  40592  dihmeetlem20N  40660  mapdpglem32  41039  diophin  41972  diophun  41973  iunrelexpuztr  42932  mullimc  44790  mullimcf  44797  addlimc  44822  fourierdlem42  45323  fourierdlem80  45360  sge0resplit  45580  hoiqssbllem3  45798