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

Theorem 19.9 1797
Description: A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (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 1778 . 2  |-  ( ph  ->  A. x ph )
3219.9h 1794 1  |-  ( E. x ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 177   E.wex 1550   F/wnf 1553
This theorem is referenced by:  exlimd  1824  excomimOLD  1881  19.19  1885  19.36  1892  19.44  1898  19.45  1899  19.41  1900  exdistrfOLD  2067  exists1  2370  dfid3  4499  fsplit  6451  a9e2ndeq  28646  e2ebind  28650  a9e2ndeqVD  29021  e2ebindVD  29024  e2ebindALT  29041  a9e2ndeqALT  29043  bnj1189  29378  exdistrfNEW7  29505  excomimOLD7  29693
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator