Theorem reeanv 3243

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-ral 3086  df-rex 3096

This theorem is referenced by:  3reeanv  3244  2reu4lem  4489  disjxiun  5110  fliftfun  7311  poseq  8154  soseq  8155  frrlem9  8291  tfrlem5  8366  uniinqs  8795  eroveu  8810  erovlem  8811  xpf1o  9127  unxpdomlem3  9218  finsschain  9316  dffi3  9391  ttrcltr  9685  rankxplim3  9853  xpnum  9937  kmlem9  10142  sornom  10261  fpwwe2lem11  10626  cnegex  11391  zaddcl  12634  rexanre  15398  o1lo1  15588  o1co  15637  rlimcn3  15641  o1of2  15664  lo1add  15678  lo1mul  15679  summo  15768  ntrivcvgmul  15956  prodmolem2  15989  prodmo  15990  dvds2lem  16326  odd2np1  16399  opoe  16421  omoe  16422  opeo  16423  omeo  16424  bezoutlem4  16600  gcddiv  16609  divgcdcoprmex  16724  pcqmul  16913  pcadd  16949  mul4sq  17014  4sqlem12  17016  prmgaplem7  17117  cyccom  19274  gaorber  19378  psgneu  19576  lsmsubm  19723  pj1eu  19766  efgredlem  19817  efgrelexlemb  19820  qusabl  19935  dprdsubg  20096  dvdsrtr  20450  unitgrp  20465  lss1d  21062  lsmspsn  21183  lspsolvlem  21244  lbsextlem2  21261  znfld  21679  cygznlem3  21688  psgnghm  21699  tgcl  23095  restbas  23284  ordtbas2  23317  uncmp  23529  txuni2  23691  txbas  23693  ptbasin  23703  txcnp  23746  txlly  23762  txnlly  23763  tx1stc  23776  tx2ndc  23777  fbasrn  24010  rnelfmlem  24078  fmfnfmlem3  24082  txflf  24132  qustgplem  24247  trust  24355  utoptop  24360  fmucndlem  24416  blin2  24555  metustto  24679  tgqioo  24926  minveclem3b  25556  pmltpc  25578  evthicc2  25588  ovolunlem2  25626  dyaddisj  25724  rolle  26118  dvcvx  26148  itgsubst  26177  plyadd  26343  plymul  26344  coeeu  26351  aalioulem6  26467  dchrptlem2  27395  lgsdchr  27485  mul2sq  27549  2sqlem5  27552  pntibnd  27723  pntlemp  27740  nosupprefixmo  27830  noinfprefixmo  27831  addsproplem2  28129  negsproplem2  28188  mulsuniflem  28308  precsexlem10  28375  zaddscl  28553  zmulscld  28556  zseo  28581  z12addscl  28636  recut  28653  readdscl  28658  remulscl  28661  cgraswap  29088  cgracom  29090  cgratr  29091  flatcgra  29092  dfcgra2  29098  acopyeu  29102  ax5seg  29229  axpasch  29232  axeuclid  29254  axcontlem4  29258  axcontlem9  29263  uhgr2edg  29499  2pthon3v  30233  pjhthmo  31595  superpos  32647  chirredi  32687  cdjreui  32725  cdj3i  32734  xrofsup  33053  archiabllem2c  33456  ccfldextdgrr  34007  ordtconnlem1  34259  dya2iocnrect  34616  txpconn  35657  cvmlift2lem10  35737  cvmlift3lem7  35750  msubco  35956  mclsppslem  36008  altopelaltxp  36401  funtransport  36456  btwnconn1lem13  36524  btwnconn1lem14  36525  segletr  36539  segleantisym  36540  funray  36565  funline  36567  tailfb  36811  mblfinlem3  38232  ismblfin  38234  itg2addnc  38247  ftc1anclem6  38271  heibor1lem  38382  crngohomfo  38579  ispridlc  38643  prter1  39577  hl2at  40103  cdlemn11pre  41908  dihord2pre  41923  dihord4  41956  dihmeetlem20N  42024  mapdpglem32  42403  diophin  43429  diophun  43430  iunrelexpuztr  44371  mullimc  46258  mullimcf  46265  addlimc  46288  fourierdlem42  46789  fourierdlem80  46826  sge0resplit  47046  hoiqssbllem3  47264