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

Theorem exdistrv 1956
Description: Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1950 and 19.42v 1954. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 2370. (Contributed by BJ, 30-Sep-2022.)
Assertion
Ref Expression
exdistrv (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem exdistrv
StepHypRef Expression
1 exdistr 1955 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.41v 1950 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
31, 2bitri 277 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 208  wa 398  wex 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781
This theorem is referenced by:  4exdistrv  1957  eu6lem  2657  2mo2  2731  reeanv  3354  cgsex2g  3517  cgsex4g  3518  vtocl2OLD  3541  spc2egv  3579  spc2ed  3581  dtru  5247  copsex2t  5359  copsex2g  5360  xpnz  5992  fununi  6405  wfrlem4  7936  wfrfun  7943  tfrlem7  7997  ener  8534  domtr  8540  unen  8574  undom  8583  sbthlem10  8614  mapen  8659  infxpenc2  9426  fseqen  9431  dfac5lem4  9530  zorn2lem6  9901  fpwwe2lem12  10041  genpnnp  10405  hashfacen  13797  summo  15054  ntrivcvgmul  15238  prodmo  15270  iscatd2  16931  gictr  18394  gsumval3eu  19003  ptbasin  22161  txcls  22188  txbasval  22190  hmphtr  22367  reconn  23412  phtpcer  23579  pcohtpy  23604  mbfi1flimlem  24305  mbfmullem  24308  itg2add  24342  brabgaf  30346  pconnconn  32486  txsconn  32496  frrlem4  33134  neibastop1  33715  bj-dtru  34147  copsex2d  34448  riscer  35302  br1cosscnvxrn  35750  sn-dtru  39223  fnchoice  41441  fzisoeu  41721  stoweidlem35  42468  elsprel  43783
  Copyright terms: Public domain W3C validator