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
Distinct variable group:   ,

Proof of Theorem 19.9v
StepHypRef Expression
1 ax5e 1727 . 2
2 19.8v 1777 . 2
31, 2impbii 188 1
 Colors of variables: wff setvar class Syntax hints:   wb 184  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