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

Theorem reeanv 3081
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 nfv 1828 . 2 𝑦𝜑
2 nfv 1828 . 2 𝑥𝜓
31, 2reean 3080 1 (∃𝑥𝐴𝑦𝐵 (𝜑𝜓) ↔ (∃𝑥𝐴 𝜑 ∧ ∃𝑦𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wa 382  wrex 2892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-ral 2896  df-rex 2897
This theorem is referenced by:  3reeanv  3082  2ralor  3083  disjxiun  4569  disjxiunOLD  4570  fliftfun  6436  tfrlem5  7336  uniinqs  7687  eroveu  7702  erovlem  7703  xpf1o  7980  unxpdomlem3  8024  unfi  8085  finsschain  8129  dffi3  8193  rankxplim3  8600  xpnum  8633  kmlem9  8836  sornom  8955  fpwwe2lem12  9315  cnegex  10064  zaddcl  11246  rexanre  13876  o1lo1  14058  o1co  14107  rlimcn2  14111  o1of2  14133  lo1add  14147  lo1mul  14148  summo  14237  ntrivcvgmul  14415  prodmolem2  14446  prodmo  14447  dvds2lem  14774  odd2np1  14845  opoe  14867  omoe  14868  opeo  14869  omeo  14870  bezoutlem4  15039  gcddiv  15048  divgcdcoprmex  15160  pcqmul  15338  pcadd  15373  mul4sq  15438  4sqlem12  15440  prmgaplem7  15541  gaorber  17506  psgneu  17691  lsmsubm  17833  pj1eu  17874  efgredlem  17925  efgrelexlemb  17928  qusabl  18033  cygabl  18057  dprdsubg  18188  dvdsrtr  18417  unitgrp  18432  lss1d  18726  lsmspsn  18847  lspsolvlem  18905  lbsextlem2  18922  znfld  19669  cygznlem3  19678  psgnghm  19686  tgcl  20522  restbas  20710  ordtbas2  20743  uncmp  20954  txuni2  21116  txbas  21118  ptbasin  21128  txcnp  21171  txlly  21187  txnlly  21188  tx1stc  21201  tx2ndc  21202  fbasrn  21436  rnelfmlem  21504  fmfnfmlem3  21508  txflf  21558  qustgplem  21672  trust  21781  utoptop  21786  fmucndlem  21843  blin2  21981  metustto  22105  tgqioo  22339  minveclem3b  22920  pmltpc  22939  evthicc2  22949  ovolunlem2  22986  dyaddisj  23083  rolle  23470  dvcvx  23500  itgsubst  23529  plyadd  23690  plymul  23691  coeeu  23698  aalioulem6  23809  dchrptlem2  24703  lgsdchr  24793  mul2sq  24857  2sqlem5  24860  pntibnd  24995  pntlemp  25012  cgraswap  25426  cgracom  25428  cgratr  25429  dfcgra2  25435  acopyeu  25439  ax5seg  25532  axpasch  25535  axeuclid  25557  axcontlem4  25561  axcontlem9  25566  usgra2edg  25673  frgrawopreglem5  26337  pjhthmo  27347  superpos  28399  chirredi  28439  cdjreui  28477  cdj3i  28486  xrofsup  28725  archiabllem2c  28882  ordtconlem1  29100  dya2iocnrect  29472  txpcon  30270  cvmlift2lem10  30350  cvmlift3lem7  30363  msubco  30484  mclsppslem  30536  poseq  30796  soseq  30797  altopelaltxp  31055  funtransport  31110  btwnconn1lem13  31178  btwnconn1lem14  31179  segletr  31193  segleantisym  31194  funray  31219  funline  31221  tailfb  31344  mblfinlem3  32417  ismblfin  32419  itg2addnc  32433  ftc1anclem6  32459  heibor1lem  32577  crngohomfo  32774  ispridlc  32838  prter1  32981  hl2at  33508  cdlemn11pre  35316  dihord2pre  35331  dihord4  35364  dihmeetlem20N  35432  mapdpglem32  35811  diophin  36153  diophun  36154  iunrelexpuztr  36829  mullimc  38483  mullimcf  38490  addlimc  38515  fourierdlem42  38842  fourierdlem80  38879  sge0resplit  39099  hoiqssbllem3  39314  2reu4a  39638  uhgr2edg  40433  2pthon3v-av  41148  frgrwopreglem5  41483
  Copyright terms: Public domain W3C validator