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

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

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 3078  df-rex 3088

This theorem is used by:  3reeanv  3236  2reu4lem  4479  disjxiun  5100  fliftfun  7320  poseq  8175  soseq  8176  frrlem9  8312  tfrlem5  8387  uniinqs  8818  eroveu  8833  erovlem  8834  xpf1o  9158  unxpdomlem3  9249  finsschain  9348  dffi3  9423  ttrcltr  9717  rankxplim3  9898  xpnum  10032  kmlem9  10237  sornom  10355  fpwwe2lem11  10726  cnegex  11491  zaddcl  12736  rexanre  15514  o1lo1  15704  o1co  15753  rlimcn3  15757  o1of2  15780  lo1add  15794  lo1mul  15795  summo  15883  ntrivcvgmul  16071  prodmolem2  16102  prodmo  16103  dvds2lem  16438  odd2np1  16511  opoe  16533  omoe  16534  opeo  16535  omeo  16536  bezoutlem4  16715  gcddiv  16724  divgcdcoprmex  16841  pcqmul  17031  pcadd  17067  mul4sq  17132  4sqlem12  17134  prmgaplem7  17235  cyccom  19418  gaorber  19522  psgneu  19720  lsmsubm  19867  pj1eu  19910  efgredlem  19961  efgrelexlemb  19964  qusabl  20079  dprdsubg  20240  dvdsrtr  20598  unitgrp  20613  crngrhmfo  20726  lss1d  21238  lsmspsn  21359  lspsolvlem  21420  lbsextlem2  21437  znfld  21866  cygznlem3  21875  psgnghm  21886  tgcl  23287  restbas  23476  ordtbas2  23509  uncmp  23721  txuni2  23884  txbas  23886  ptbasin  23896  txcnp  23939  txlly  23955  txnlly  23956  tx1stc  23969  tx2ndc  23970  fbasrn  24203  rnelfmlem  24271  fmfnfmlem3  24275  txflf  24325  qustgplem  24440  trust  24548  utoptop  24553  fmucndlem  24609  blin2  24748  metustto  24872  tgqioo  25119  minveclem3b  25749  pmltpc  25771  evthicc2  25781  ovolunlem2  25819  dyaddisj  25917  rolle  26310  dvcvx  26340  itgsubst  26369  plyadd  26536  plymul  26537  coeeu  26544  aalioulem6  26664  dchrptlem2  27592  lgsdchr  27682  mul2sq  27746  2sqlem5  27749  pntibnd  27920  pntlemp  27937  nosupprefixmo  28057  noinfprefixmo  28058  addsproplem2  28356  negsproplem2  28415  mulsuniflem  28535  precsexlem10  28602  zaddscl  28780  zmulscld  28783  zseo  28808  z12addscl  28863  recut  28880  readdscl  28885  remulscl  28888  cgraswap  29327  cgracom  29329  cgratr  29330  flatcgra  29332  dfcgra2  29338  acopyeu  29342  ax5seg  29516  axpasch  29519  axeuclid  29541  axcontlem4  29545  axcontlem9  29550  uhgr2edg  29789  2pthon3v  30532  pjhthmo  31904  superpos  32956  chirredi  32996  cdjreui  33034  cdj3i  33043  xrofsup  33359  archiabllem2c  33756  ccfldextdgrr  34304  ordtconnlem1  34556  dya2iocnrect  34913  txpconn  35997  cvmlift2lem10  36077  cvmlift3lem7  36090  msubco  36296  mclsppslem  36348  altopelaltxp  36741  funtransport  36796  btwnconn1lem13  36864  btwnconn1lem14  36865  segletr  36879  segleantisym  36880  funray  36905  funline  36907  tailfb  37165  mblfinlem3  38577  ismblfin  38579  itg2addnc  38592  ftc1anclem6  38616  heibor1lem  38743  crngohomfo  38940  ispridlc  39004  prter1  39936  hl2at  40462  cdlemn11pre  42267  dihord2pre  42282  dihord4  42315  dihmeetlem20N  42383  mapdpglem32  42762  diophin  43782  diophun  43783  iunrelexpuztr  44718  mullimc  46627  mullimcf  46634  addlimc  46657  fourierdlem42  47158  fourierdlem80  47195  sge0resplit  47415  hoiqssbllem3  47633