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

Theorem 19.9 1783
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.)
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 . 2  |-  F/ x ph
2 19.9t 1782 . 2  |-  ( F/ x ph  ->  ( E. x ph  <->  ph ) )
31, 2ax-mp 8 1  |-  ( E. x ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1528   F/wnf 1531
This theorem is referenced by:  excomim  1785  19.19  1789  19.36  1807  19.44  1813  19.45  1814  exdistrf  1911  exists1  2232  dfid3  4310  fsplit  6223  a9e2ndeq  28325  e2ebind  28329  a9e2ndeqVD  28685  e2ebindVD  28688  e2ebindALT  28706  a9e2ndeqALT  28708  bnj1131  28819  bnj1397  28867  bnj1189  29039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator