Theorem reeanv 3210

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  3reeanv  3211  2reu4lem  4464  disjxiun  5083  fliftfun  7261  poseq  8102  soseq  8103  frrlem9  8238  tfrlem5  8313  uniinqs  8738  eroveu  8753  erovlem  8754  xpf1o  9071  unxpdomlem3  9162  finsschain  9263  dffi3  9338  ttrcltr  9631  rankxplim3  9799  xpnum  9869  kmlem9  10075  sornom  10193  fpwwe2lem11  10558  cnegex  11321  zaddcl  12561  rexanre  15303  o1lo1  15493  o1co  15542  rlimcn3  15546  o1of2  15569  lo1add  15583  lo1mul  15584  summo  15673  ntrivcvgmul  15861  prodmolem2  15894  prodmo  15895  dvds2lem  16231  odd2np1  16304  opoe  16326  omoe  16327  opeo  16328  omeo  16329  bezoutlem4  16505  gcddiv  16514  divgcdcoprmex  16629  pcqmul  16818  pcadd  16854  mul4sq  16919  4sqlem12  16921  prmgaplem7  17022  cyccom  19172  gaorber  19277  psgneu  19475  lsmsubm  19622  pj1eu  19665  efgredlem  19716  efgrelexlemb  19719  qusabl  19834  dprdsubg  19995  dvdsrtr  20342  unitgrp  20357  lss1d  20952  lsmspsn  21074  lspsolvlem  21135  lbsextlem2  21152  znfld  21553  cygznlem3  21562  psgnghm  21573  tgcl  22947  restbas  23136  ordtbas2  23169  uncmp  23381  txuni2  23543  txbas  23545  ptbasin  23555  txcnp  23598  txlly  23614  txnlly  23615  tx1stc  23628  tx2ndc  23629  fbasrn  23862  rnelfmlem  23930  fmfnfmlem3  23934  txflf  23984  qustgplem  24099  trust  24207  utoptop  24212  fmucndlem  24268  blin2  24407  metustto  24531  tgqioo  24778  minveclem3b  25408  pmltpc  25430  evthicc2  25440  ovolunlem2  25478  dyaddisj  25576  rolle  25970  dvcvx  26000  itgsubst  26029  plyadd  26195  plymul  26196  coeeu  26203  aalioulem6  26317  dchrptlem2  27245  lgsdchr  27335  mul2sq  27399  2sqlem5  27402  pntibnd  27573  pntlemp  27590  nosupprefixmo  27681  noinfprefixmo  27682  addsproplem2  27979  negsproplem2  28038  mulsuniflem  28158  precsexlem10  28225  zaddscl  28403  zmulscld  28406  zseo  28431  z12addscl  28486  recut  28503  readdscl  28508  remulscl  28511  cgraswap  28905  cgracom  28907  cgratr  28908  flatcgra  28909  dfcgra2  28915  acopyeu  28919  ax5seg  29024  axpasch  29027  axeuclid  29049  axcontlem4  29053  axcontlem9  29058  uhgr2edg  29294  2pthon3v  30029  pjhthmo  31391  superpos  32443  chirredi  32483  cdjreui  32521  cdj3i  32530  xrofsup  32858  archiabllem2c  33274  ccfldextdgrr  33835  ordtconnlem1  34087  dya2iocnrect  34444  txpconn  35433  cvmlift2lem10  35513  cvmlift3lem7  35526  msubco  35732  mclsppslem  35784  altopelaltxp  36177  funtransport  36232  btwnconn1lem13  36300  btwnconn1lem14  36301  segletr  36315  segleantisym  36316  funray  36341  funline  36343  tailfb  36578  mblfinlem3  37997  ismblfin  37999  itg2addnc  38012  ftc1anclem6  38036  heibor1lem  38147  crngohomfo  38344  ispridlc  38408  prter1  39342  hl2at  39868  cdlemn11pre  41673  dihord2pre  41688  dihord4  41721  dihmeetlem20N  41789  mapdpglem32  42168  diophin  43221  diophun  43222  iunrelexpuztr  44167  mullimc  46067  mullimcf  46074  addlimc  46097  fourierdlem42  46598  fourierdlem80  46635  sge0resplit  46855  hoiqssbllem3  47073