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

Theorem 19.9 1785
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 1784 . 2  |-  ( F/ x ph  ->  ( E. x ph  <->  ph ) )
31, 2ax-mp 10 1  |-  ( E. x ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1529   F/wnf 1532
This theorem is referenced by:  excomim  1787  19.19  1791  19.36  1809  19.44  1815  19.45  1816  exdistrf  1914  exists1  2234  dfid3  4310  fsplit  6185  a9e2ndeq  27597  e2ebind  27601  a9e2ndeqVD  27954  e2ebindVD  27957  e2ebindALT  27975  a9e2ndeqALT  27977  bnj1131  28087  bnj1397  28135  bnj1189  28307
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator