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

Theorem 19.42v 1915
Description: Version of 19.42 2103 with a dv condition requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
19.42v (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem 19.42v
StepHypRef Expression
1 19.41v 1911 . 2 (∃𝑥(𝜓𝜑) ↔ (∃𝑥𝜓𝜑))
2 exancom 1784 . 2 (∃𝑥(𝜑𝜓) ↔ ∃𝑥(𝜓𝜑))
3 ancom 466 . 2 ((𝜑 ∧ ∃𝑥𝜓) ↔ (∃𝑥𝜓𝜑))
41, 2, 33bitr4i 292 1 (∃𝑥(𝜑𝜓) ↔ (𝜑 ∧ ∃𝑥𝜓))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702
This theorem is referenced by:  exdistr  1916  19.42vv  1917  19.42vvv  1918  4exdistr  1921  eeeanv  2182  2sb5  2442  rexcom4a  3215  ceqsex2  3233  reuind  3397  2reu5lem3  3401  sbccomlem  3494  bm1.3ii  4749  eqvinop  4920  dmopabss  5301  dmopab3  5302  mptpreima  5592  mptfnf  5977  brprcneu  6146  fndmin  6285  fliftf  6525  dfoprab2  6661  dmoprab  6701  dmoprabss  6702  fnoprabg  6721  uniuni  6927  zfrep6  7088  opabex3d  7098  opabex3  7099  fsplit  7234  eroveu  7794  rankuni  8678  aceq1  8892  dfac3  8896  kmlem14  8937  kmlem15  8938  axdc2lem  9222  1idpr  9803  ltexprlem1  9810  ltexprlem4  9813  xpcogend  13655  shftdm  13753  joindm  16935  meetdm  16949  ntreq0  20804  cnextf  21793  fusgr2wsp2nb  27073  adjeu  28618  rexunirn  29202  fpwrelmapffslem  29373  bnj1019  30593  bnj1209  30610  bnj1033  30780  bnj1189  30820  dfiota3  31707  brimg  31721  funpartlem  31726  bj-eeanvw  32381  bj-rexcom4  32551  bj-rexcom4a  32552  bj-snsetex  32633  bj-snglc  32639  bj-restuni  32722  bj-toprntopon  32735  itg2addnc  33131  sbccom2lem  33596  rp-isfinite6  37380  undmrnresiss  37426  elintima  37461  pm11.58  38107  pm11.71  38114  2sbc5g  38134  iotasbc2  38138  ax6e2nd  38291  ax6e2ndVD  38662  ax6e2ndALT  38684  stoweidlem60  39610  elpglem3  41775
  Copyright terms: Public domain W3C validator