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

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

Proof of Theorem exdistrv
StepHypRef Expression
1 exdistr 1959 . 2 (∃𝑥𝑦(𝜑𝜓) ↔ ∃𝑥(𝜑 ∧ ∃𝑦𝜓))
2 19.41v 1954 . 2 (∃𝑥(𝜑 ∧ ∃𝑦𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
31, 2bitri 275 1 (∃𝑥𝑦(𝜑𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  4exdistrv  1961  eu6lem  2572  2mo2  2648  reeanv  3220  cgsex2g  3492  cgsex4g  3493  cgsex4gOLD  3494  spc2egv  3561  spc2ed  3563  dtruALT2  5330  exexneq  5396  dtruOLD  5403  copsex2t  5454  copsex2gOLD  5456  xpnz  6116  fununi  6581  frrlem4  8225  wfrlem4OLD  8263  wfrfunOLD  8270  tfrlem7  8334  ener  8948  domtr  8954  unen  8997  undom  9010  undomOLD  9011  sbthlem10  9043  mapen  9092  entrfil  9139  domtrfil  9146  sbthfilem  9152  infxpenc2  9965  fseqen  9970  dfac5lem4  10069  zorn2lem6  10444  fpwwe2lem11  10584  genpnnp  10948  hashfacen  14358  hashfacenOLD  14359  summo  15609  ntrivcvgmul  15794  prodmo  15826  iscatd2  17568  catcone0  17574  gictr  19072  gsumval3eu  19688  ptbasin  22944  txcls  22971  txbasval  22973  hmphtr  23150  reconn  24207  phtpcer  24374  pcohtpy  24399  mbfi1flimlem  25103  mbfmullem  25106  itg2add  25140  brabgaf  31569  pconnconn  33865  txsconn  33875  neibastop1  34860  bj-unexg  35538  copsex2d  35639  riscer  36476  disjecxrn  36880  br1cosscnvxrn  36965  rictr  40731  fnchoice  43308  fzisoeu  43608  stoweidlem35  44350  elsprel  45741
  Copyright terms: Public domain W3C validator