Theorem reeanv 3239

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 3238	1 ⊢ (∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝜑 ∧ 𝜓) ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃𝑦 ∈ 𝐵 𝜓))

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

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 3082  df-rex 3092

This theorem is used by:  3reeanv  3240  2reu4lem  4486  disjxiun  5108  fliftfun  7319  poseq  8160  soseq  8161  frrlem9  8297  tfrlem5  8372  uniinqs  8801  eroveu  8816  erovlem  8817  xpf1o  9134  unxpdomlem3  9225  finsschain  9323  dffi3  9398  ttrcltr  9692  rankxplim3  9860  xpnum  9953  kmlem9  10158  sornom  10276  fpwwe2lem11  10645  cnegex  11410  zaddcl  12653  rexanre  15426  o1lo1  15616  o1co  15665  rlimcn3  15669  o1of2  15692  lo1add  15706  lo1mul  15707  summo  15795  ntrivcvgmul  15983  prodmolem2  16016  prodmo  16017  dvds2lem  16352  odd2np1  16425  opoe  16447  omoe  16448  opeo  16449  omeo  16450  bezoutlem4  16626  gcddiv  16635  divgcdcoprmex  16750  pcqmul  16939  pcadd  16975  mul4sq  17040  4sqlem12  17042  prmgaplem7  17143  cyccom  19322  gaorber  19426  psgneu  19624  lsmsubm  19771  pj1eu  19814  efgredlem  19865  efgrelexlemb  19868  qusabl  19983  dprdsubg  20144  dvdsrtr  20500  unitgrp  20515  crngrhmfo  20628  lss1d  21138  lsmspsn  21259  lspsolvlem  21320  lbsextlem2  21337  znfld  21764  cygznlem3  21773  psgnghm  21784  tgcl  23180  restbas  23369  ordtbas2  23402  uncmp  23614  txuni2  23777  txbas  23779  ptbasin  23789  txcnp  23832  txlly  23848  txnlly  23849  tx1stc  23862  tx2ndc  23863  fbasrn  24096  rnelfmlem  24164  fmfnfmlem3  24168  txflf  24218  qustgplem  24333  trust  24441  utoptop  24446  fmucndlem  24502  blin2  24641  metustto  24765  tgqioo  25012  minveclem3b  25642  pmltpc  25664  evthicc2  25674  ovolunlem2  25712  dyaddisj  25810  rolle  26204  dvcvx  26234  itgsubst  26263  plyadd  26429  plymul  26430  coeeu  26437  aalioulem6  26555  dchrptlem2  27484  lgsdchr  27574  mul2sq  27638  2sqlem5  27641  pntibnd  27812  pntlemp  27829  nosupprefixmo  27919  noinfprefixmo  27920  addsproplem2  28218  negsproplem2  28277  mulsuniflem  28397  precsexlem10  28464  zaddscl  28642  zmulscld  28645  zseo  28670  z12addscl  28725  recut  28742  readdscl  28747  remulscl  28750  cgraswap  29186  cgracom  29188  cgratr  29189  flatcgra  29190  dfcgra2  29196  acopyeu  29200  ax5seg  29347  axpasch  29350  axeuclid  29372  axcontlem4  29376  axcontlem9  29381  uhgr2edg  29620  2pthon3v  30363  pjhthmo  31729  superpos  32781  chirredi  32821  cdjreui  32859  cdj3i  32868  xrofsup  33186  archiabllem2c  33583  ccfldextdgrr  34130  ordtconnlem1  34382  dya2iocnrect  34740  txpconn  35765  cvmlift2lem10  35845  cvmlift3lem7  35858  msubco  36064  mclsppslem  36116  altopelaltxp  36509  funtransport  36564  btwnconn1lem13  36632  btwnconn1lem14  36633  segletr  36647  segleantisym  36648  funray  36673  funline  36675  tailfb  36949  mblfinlem3  38371  ismblfin  38373  itg2addnc  38386  ftc1anclem6  38410  heibor1lem  38522  crngohomfo  38719  ispridlc  38783  prter1  39715  hl2at  40241  cdlemn11pre  42046  dihord2pre  42061  dihord4  42094  dihmeetlem20N  42162  mapdpglem32  42541  diophin  43580  diophun  43581  iunrelexpuztr  44522  mullimc  46409  mullimcf  46416  addlimc  46439  fourierdlem42  46940  fourierdlem80  46977  sge0resplit  47197  hoiqssbllem3  47415