Theorem reeanv 3215

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

Syntax hints:   ↔ wb 205   ∧ wa 396   ∈ wcel 2106  ∃wrex 3069

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-ral 3061  df-rex 3070

This theorem is referenced by:  3reeanv  3216  2ralorOLD  3218  2reu4lem  4488  disjxiun  5107  fliftfun  7262  poseq  8095  soseq  8096  frrlem9  8230  tfrlem5  8331  uniinqs  8743  eroveu  8758  erovlem  8759  xpf1o  9090  unxpdomlem3  9203  unfiOLD  9264  finsschain  9310  dffi3  9376  ttrcltr  9661  rankxplim3  9826  xpnum  9896  kmlem9  10103  sornom  10222  fpwwe2lem11  10586  cnegex  11345  zaddcl  12552  rexanre  15243  o1lo1  15431  o1co  15480  rlimcn3  15484  o1of2  15507  lo1add  15521  lo1mul  15522  summo  15613  ntrivcvgmul  15798  prodmolem2  15829  prodmo  15830  dvds2lem  16162  odd2np1  16234  opoe  16256  omoe  16257  opeo  16258  omeo  16259  bezoutlem4  16434  gcddiv  16443  divgcdcoprmex  16553  pcqmul  16736  pcadd  16772  mul4sq  16837  4sqlem12  16839  prmgaplem7  16940  cyccom  19010  gaorber  19102  psgneu  19302  lsmsubm  19449  pj1eu  19492  efgredlem  19543  efgrelexlemb  19546  qusabl  19657  dprdsubg  19817  dvdsrtr  20095  unitgrp  20110  lss1d  20481  lsmspsn  20602  lspsolvlem  20662  lbsextlem2  20679  znfld  21004  cygznlem3  21013  psgnghm  21021  tgcl  22356  restbas  22546  ordtbas2  22579  uncmp  22791  txuni2  22953  txbas  22955  ptbasin  22965  txcnp  23008  txlly  23024  txnlly  23025  tx1stc  23038  tx2ndc  23039  fbasrn  23272  rnelfmlem  23340  fmfnfmlem3  23344  txflf  23394  qustgplem  23509  trust  23618  utoptop  23623  fmucndlem  23680  blin2  23819  metustto  23946  tgqioo  24200  minveclem3b  24829  pmltpc  24851  evthicc2  24861  ovolunlem2  24899  dyaddisj  24997  rolle  25391  dvcvx  25421  itgsubst  25450  plyadd  25615  plymul  25616  coeeu  25623  aalioulem6  25734  dchrptlem2  26650  lgsdchr  26740  mul2sq  26804  2sqlem5  26807  pntibnd  26978  pntlemp  26995  nosupprefixmo  27085  noinfprefixmo  27086  addsproplem2  27325  negsproplem2  27370  cgraswap  27825  cgracom  27827  cgratr  27828  flatcgra  27829  dfcgra2  27835  acopyeu  27839  ax5seg  27950  axpasch  27953  axeuclid  27975  axcontlem4  27979  axcontlem9  27984  uhgr2edg  28219  2pthon3v  28951  pjhthmo  30307  superpos  31359  chirredi  31399  cdjreui  31437  cdj3i  31446  xrofsup  31740  archiabllem2c  32101  ccfldextdgrr  32443  ordtconnlem1  32594  dya2iocnrect  32970  txpconn  33913  cvmlift2lem10  33993  cvmlift3lem7  34006  msubco  34212  mclsppslem  34264  altopelaltxp  34637  funtransport  34692  btwnconn1lem13  34760  btwnconn1lem14  34761  segletr  34775  segleantisym  34776  funray  34801  funline  34803  tailfb  34925  mblfinlem3  36190  ismblfin  36192  itg2addnc  36205  ftc1anclem6  36229  heibor1lem  36341  crngohomfo  36538  ispridlc  36602  prter1  37414  hl2at  37941  cdlemn11pre  39746  dihord2pre  39761  dihord4  39794  dihmeetlem20N  39862  mapdpglem32  40241  diophin  41153  diophun  41154  iunrelexpuztr  42113  mullimc  43977  mullimcf  43984  addlimc  44009  fourierdlem42  44510  fourierdlem80  44547  sge0resplit  44767  hoiqssbllem3  44985