Theorem reeanv 3229

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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071

This theorem is referenced by:  3reeanv  3230  2ralorOLD  3232  2reu4lem  4522  disjxiun  5140  fliftfun  7332  poseq  8183  soseq  8184  frrlem9  8319  tfrlem5  8420  uniinqs  8837  eroveu  8852  erovlem  8853  xpf1o  9179  unxpdomlem3  9288  finsschain  9399  dffi3  9471  ttrcltr  9756  rankxplim3  9921  xpnum  9991  kmlem9  10199  sornom  10317  fpwwe2lem11  10681  cnegex  11442  zaddcl  12657  rexanre  15385  o1lo1  15573  o1co  15622  rlimcn3  15626  o1of2  15649  lo1add  15663  lo1mul  15664  summo  15753  ntrivcvgmul  15938  prodmolem2  15971  prodmo  15972  dvds2lem  16306  odd2np1  16378  opoe  16400  omoe  16401  opeo  16402  omeo  16403  bezoutlem4  16579  gcddiv  16588  divgcdcoprmex  16703  pcqmul  16891  pcadd  16927  mul4sq  16992  4sqlem12  16994  prmgaplem7  17095  cyccom  19221  gaorber  19326  psgneu  19524  lsmsubm  19671  pj1eu  19714  efgredlem  19765  efgrelexlemb  19768  qusabl  19883  dprdsubg  20044  dvdsrtr  20368  unitgrp  20383  lss1d  20961  lsmspsn  21083  lspsolvlem  21144  lbsextlem2  21161  znfld  21579  cygznlem3  21588  psgnghm  21598  tgcl  22976  restbas  23166  ordtbas2  23199  uncmp  23411  txuni2  23573  txbas  23575  ptbasin  23585  txcnp  23628  txlly  23644  txnlly  23645  tx1stc  23658  tx2ndc  23659  fbasrn  23892  rnelfmlem  23960  fmfnfmlem3  23964  txflf  24014  qustgplem  24129  trust  24238  utoptop  24243  fmucndlem  24300  blin2  24439  metustto  24566  tgqioo  24821  minveclem3b  25462  pmltpc  25485  evthicc2  25495  ovolunlem2  25533  dyaddisj  25631  rolle  26028  dvcvx  26059  itgsubst  26090  plyadd  26256  plymul  26257  coeeu  26264  aalioulem6  26379  dchrptlem2  27309  lgsdchr  27399  mul2sq  27463  2sqlem5  27466  pntibnd  27637  pntlemp  27654  nosupprefixmo  27745  noinfprefixmo  27746  addsproplem2  28003  negsproplem2  28061  mulsuniflem  28175  precsexlem10  28240  zaddscl  28380  zmulscld  28383  zseo  28406  recut  28428  readdscl  28431  remulscl  28434  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  dfcgra2  28838  acopyeu  28842  ax5seg  28953  axpasch  28956  axeuclid  28978  axcontlem4  28982  axcontlem9  28987  uhgr2edg  29225  2pthon3v  29963  pjhthmo  31321  superpos  32373  chirredi  32413  cdjreui  32451  cdj3i  32460  xrofsup  32771  archiabllem2c  33202  ccfldextdgrr  33722  ordtconnlem1  33923  dya2iocnrect  34283  txpconn  35237  cvmlift2lem10  35317  cvmlift3lem7  35330  msubco  35536  mclsppslem  35588  altopelaltxp  35977  funtransport  36032  btwnconn1lem13  36100  btwnconn1lem14  36101  segletr  36115  segleantisym  36116  funray  36141  funline  36143  tailfb  36378  mblfinlem3  37666  ismblfin  37668  itg2addnc  37681  ftc1anclem6  37705  heibor1lem  37816  crngohomfo  38013  ispridlc  38077  prter1  38880  hl2at  39407  cdlemn11pre  41212  dihord2pre  41227  dihord4  41260  dihmeetlem20N  41328  mapdpglem32  41707  diophin  42783  diophun  42784  iunrelexpuztr  43732  mullimc  45631  mullimcf  45638  addlimc  45663  fourierdlem42  46164  fourierdlem80  46201  sge0resplit  46421  hoiqssbllem3  46639