MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  19.9v Structured version   Unicode version

Theorem 19.9v 1778
Description: Version of 19.9 1916 with a dv condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 1779. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 1814. (Revised by Wolf Lammen, 4-Dec-2017.)
Assertion
Ref Expression
19.9v  |-  ( E. x ph  <->  ph )
Distinct variable group:    ph, x

Proof of Theorem 19.9v
StepHypRef Expression
1 ax5e 1727 . 2  |-  ( E. x ph  ->  ph )
2 19.8v 1777 . 2  |-  ( ph  ->  E. x ph )
31, 2impbii 188 1  |-  ( E. x ph  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771
This theorem depends on definitions:  df-bi 185  df-ex 1634
This theorem is referenced by:  19.3v  1779  19.23v  1784  19.36v  1786  19.44v  1794  19.41v  1795  zfcndpow  8944  elsnxp  27786  volfiniune  28559  bnj937  29038  bnj594  29178  bnj907  29231  bnj1128  29254  bnj1145  29257  prter2  31885  relopabVD  36713  rfcnnnub  36772
  Copyright terms: Public domain W3C validator