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

Theorem 19.9 1795
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 1794 . 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 1531   F/wnf 1534
This theorem is referenced by:  excomim  1797  19.19  1801  19.36  1819  19.44  1825  19.45  1826  exdistrf  1924  exists1  2245  dfid3  4326  fsplit  6239  a9e2ndeq  28624  e2ebind  28628  a9e2ndeqVD  29001  e2ebindVD  29004  e2ebindALT  29022  a9e2ndeqALT  29024  bnj1131  29135  bnj1397  29183  bnj1189  29355  exdistrfNEW7  29482  excomimOLD7  29647
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator