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

Theorem 19.9v 1984
Description: Version of 19.9 2201 with a disjoint variable condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 1982. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 2011. (Revised by Wolf Lammen, 4-Dec-2017.)
Assertion
Ref Expression
19.9v (∃𝑥𝜑𝜑)
Distinct variable group:   𝜑,𝑥

Proof of Theorem 19.9v
StepHypRef Expression
1 ax5e 1909 . 2 (∃𝑥𝜑𝜑)
2 19.8v 1983 . 2 (𝜑 → ∃𝑥𝜑)
31, 2impbii 211 1 (∃𝑥𝜑𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 208  wex 1776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966
This theorem depends on definitions:  df-bi 209  df-ex 1777
This theorem is referenced by:  19.3vOLD  1985  19.36v  1990  19.44v  1995  19.45v  1996  zfcndpow  10037  volfiniune  31489  bnj937  32043  bnj594  32184  bnj907  32239  bnj1128  32262  bnj1145  32265  coss0  35718  prter2  36016  relopabVD  41235  rfcnnnub  41293
  Copyright terms: Public domain W3C validator