Theorem reeanv 3234

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3077  df-rex 3087

This theorem is used by:  3reeanv  3235  2reu4lem  4479  disjxiun  5100  fliftfun  7314  poseq  8157  soseq  8158  frrlem9  8294  tfrlem5  8369  uniinqs  8800  eroveu  8815  erovlem  8816  xpf1o  9140  unxpdomlem3  9231  finsschain  9329  dffi3  9404  ttrcltr  9698  rankxplim3  9866  xpnum  9959  kmlem9  10164  sornom  10282  fpwwe2lem11  10653  cnegex  11418  zaddcl  12661  rexanre  15437  o1lo1  15627  o1co  15676  rlimcn3  15680  o1of2  15703  lo1add  15717  lo1mul  15718  summo  15806  ntrivcvgmul  15994  prodmolem2  16025  prodmo  16026  dvds2lem  16361  odd2np1  16434  opoe  16456  omoe  16457  opeo  16458  omeo  16459  bezoutlem4  16635  gcddiv  16644  divgcdcoprmex  16759  pcqmul  16948  pcadd  16984  mul4sq  17049  4sqlem12  17051  prmgaplem7  17152  cyccom  19334  gaorber  19438  psgneu  19636  lsmsubm  19783  pj1eu  19826  efgredlem  19877  efgrelexlemb  19880  qusabl  19995  dprdsubg  20156  dvdsrtr  20512  unitgrp  20527  crngrhmfo  20640  lss1d  21150  lsmspsn  21271  lspsolvlem  21332  lbsextlem2  21349  znfld  21776  cygznlem3  21785  psgnghm  21796  tgcl  23197  restbas  23386  ordtbas2  23419  uncmp  23631  txuni2  23794  txbas  23796  ptbasin  23806  txcnp  23849  txlly  23865  txnlly  23866  tx1stc  23879  tx2ndc  23880  fbasrn  24113  rnelfmlem  24181  fmfnfmlem3  24185  txflf  24235  qustgplem  24350  trust  24458  utoptop  24463  fmucndlem  24519  blin2  24658  metustto  24782  tgqioo  25029  minveclem3b  25659  pmltpc  25681  evthicc2  25691  ovolunlem2  25729  dyaddisj  25827  rolle  26220  dvcvx  26250  itgsubst  26279  plyadd  26446  plymul  26447  coeeu  26454  aalioulem6  26576  dchrptlem2  27504  lgsdchr  27594  mul2sq  27658  2sqlem5  27661  pntibnd  27832  pntlemp  27849  nosupprefixmo  27939  noinfprefixmo  27940  addsproplem2  28238  negsproplem2  28297  mulsuniflem  28417  precsexlem10  28484  zaddscl  28662  zmulscld  28665  zseo  28690  z12addscl  28745  recut  28762  readdscl  28767  remulscl  28770  cgraswap  29209  cgracom  29211  cgratr  29212  flatcgra  29214  dfcgra2  29220  acopyeu  29224  ax5seg  29398  axpasch  29401  axeuclid  29423  axcontlem4  29427  axcontlem9  29432  uhgr2edg  29671  2pthon3v  30414  pjhthmo  31786  superpos  32838  chirredi  32878  cdjreui  32916  cdj3i  32925  xrofsup  33241  archiabllem2c  33638  ccfldextdgrr  34185  ordtconnlem1  34437  dya2iocnrect  34795  txpconn  35814  cvmlift2lem10  35894  cvmlift3lem7  35907  msubco  36113  mclsppslem  36165  altopelaltxp  36559  funtransport  36614  btwnconn1lem13  36682  btwnconn1lem14  36683  segletr  36697  segleantisym  36698  funray  36723  funline  36725  tailfb  36999  mblfinlem3  38411  ismblfin  38413  itg2addnc  38426  ftc1anclem6  38450  heibor1lem  38562  crngohomfo  38759  ispridlc  38823  prter1  39755  hl2at  40281  cdlemn11pre  42086  dihord2pre  42101  dihord4  42134  dihmeetlem20N  42202  mapdpglem32  42581  diophin  43620  diophun  43621  iunrelexpuztr  44562  mullimc  46449  mullimcf  46456  addlimc  46479  fourierdlem42  46980  fourierdlem80  47017  sge0resplit  47237  hoiqssbllem3  47455