MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reeanv Structured version   Visualization version   GIF version

Theorem reeanv 3365
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
StepHypRef Expression
1 exdistrv 1947 . 2 (∃𝑥𝑦((𝑥𝐴𝜑) ∧ (𝑦𝐵𝜓)) ↔ (∃𝑥(𝑥𝐴𝜑) ∧ ∃𝑦(𝑦𝐵𝜓)))
21reeanlem 3363 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  3reeanv  3366  2ralor  3367  2reu4lem  4461  disjxiun  5054  fliftfun  7054  tfrlem5  8005  uniinqs  8366  eroveu  8381  erovlem  8382  xpf1o  8667  unxpdomlem3  8712  unfi  8773  finsschain  8819  dffi3  8883  rankxplim3  9298  xpnum  9368  kmlem9  9572  sornom  9687  fpwwe2lem12  10051  cnegex  10809  zaddcl  12010  rexanre  14694  o1lo1  14882  o1co  14931  rlimcn2  14935  o1of2  14957  lo1add  14971  lo1mul  14972  summo  15062  ntrivcvgmul  15246  prodmolem2  15277  prodmo  15278  dvds2lem  15610  odd2np1  15678  opoe  15700  omoe  15701  opeo  15702  omeo  15703  bezoutlem4  15878  gcddiv  15887  divgcdcoprmex  15998  pcqmul  16178  pcadd  16213  mul4sq  16278  4sqlem12  16280  prmgaplem7  16381  cyccom  18284  gaorber  18376  psgneu  18563  lsmsubm  18707  pj1eu  18751  efgredlem  18802  efgrelexlemb  18805  qusabl  18914  cygablOLD  18940  dprdsubg  19075  dvdsrtr  19331  unitgrp  19346  lss1d  19664  lsmspsn  19785  lspsolvlem  19843  lbsextlem2  19860  znfld  20635  cygznlem3  20644  psgnghm  20652  tgcl  21505  restbas  21694  ordtbas2  21727  uncmp  21939  txuni2  22101  txbas  22103  ptbasin  22113  txcnp  22156  txlly  22172  txnlly  22173  tx1stc  22186  tx2ndc  22187  fbasrn  22420  rnelfmlem  22488  fmfnfmlem3  22492  txflf  22542  qustgplem  22656  trust  22765  utoptop  22770  fmucndlem  22827  blin2  22966  metustto  23090  tgqioo  23335  minveclem3b  23958  pmltpc  23978  evthicc2  23988  ovolunlem2  24026  dyaddisj  24124  rolle  24514  dvcvx  24544  itgsubst  24573  plyadd  24734  plymul  24735  coeeu  24742  aalioulem6  24853  dchrptlem2  25768  lgsdchr  25858  mul2sq  25922  2sqlem5  25925  pntibnd  26096  pntlemp  26113  cgraswap  26533  cgracom  26535  cgratr  26536  flatcgra  26537  dfcgra2  26543  acopyeu  26547  ax5seg  26651  axpasch  26654  axeuclid  26676  axcontlem4  26680  axcontlem9  26685  uhgr2edg  26917  2pthon3v  27649  pjhthmo  29006  superpos  30058  chirredi  30098  cdjreui  30136  cdj3i  30145  xrofsup  30418  archiabllem2c  30751  ccfldextdgrr  30956  ordtconnlem1  31066  dya2iocnrect  31438  txpconn  32376  cvmlift2lem10  32456  cvmlift3lem7  32469  msubco  32675  mclsppslem  32727  poseq  32992  soseq  32993  frrlem9  33028  noprefixmo  33099  altopelaltxp  33334  funtransport  33389  btwnconn1lem13  33457  btwnconn1lem14  33458  segletr  33472  segleantisym  33473  funray  33498  funline  33500  tailfb  33622  mblfinlem3  34812  ismblfin  34814  itg2addnc  34827  ftc1anclem6  34853  heibor1lem  34968  crngohomfo  35165  ispridlc  35229  prter1  35895  hl2at  36421  cdlemn11pre  38226  dihord2pre  38241  dihord4  38274  dihmeetlem20N  38342  mapdpglem32  38721  diophin  39247  diophun  39248  iunrelexpuztr  39942  mullimc  41773  mullimcf  41780  addlimc  41805  fourierdlem42  42311  fourierdlem80  42348  sge0resplit  42565  hoiqssbllem3  42783
  Copyright terms: Public domain W3C validator