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

Theorem 19.9v 1754
 Description: Version of 19.9 1893 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 1755. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 1790. (Revised by Wolf Lammen, 4-Dec-2017.)
Assertion
Ref Expression
19.9v
Distinct variable group:   ,

Proof of Theorem 19.9v
StepHypRef Expression
1 ax5e 1706 . 2
2 19.8v 1753 . 2
31, 2impbii 188 1
 Colors of variables: wff setvar class Syntax hints:  <->wb 184  E.wex 1612 This theorem is referenced by:  19.3v  1755  19.23v  1760  19.36v  1762  19.44v  1770  19.41v  1771  zfcndpow  9015  volfiniune  28202  prter2  30622  rfcnnnub  31411  relopabVD  33701  bnj937  33830  bnj594  33970  bnj907  34023  bnj1128  34046  bnj1145  34049 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747 This theorem depends on definitions:  df-bi 185  df-ex 1613
 Copyright terms: Public domain W3C validator