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

Theorem 19.9 1898
Description: A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. See 19.9v 1759 for a version requiring fewer axioms. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)
Hypothesis
Ref Expression
19.9.1  |-  F/ x ph
Assertion
Ref Expression
19.9  |-  ( E. x ph  <->  ph )

Proof of Theorem 19.9
StepHypRef Expression
1 19.9.1 . . 3  |-  F/ x ph
21nfri 1879 . 2  |-  ( ph  ->  A. x ph )
3219.9h 1896 1  |-  ( E. x ph  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1617   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  exlimd  1919  19.19  1964  19.36  1969  19.44  1974  19.45  1975  19.41  1976  exists1  2385  dfid3  4785  fsplit  6878  ax6e2ndeq  33726  e2ebind  33730  ax6e2ndeqVD  34110  e2ebindVD  34113  e2ebindALT  34130  ax6e2ndeqALT  34132  bnj1189  34466  bj-exexbiex  34655  bj-exalbial  34657
  Copyright terms: Public domain W3C validator