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

Theorem 19.9 1762
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 1761 . 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 1537   F/wnf 1539
This theorem is referenced by:  excomim  1764  19.19  1769  19.36  1788  19.44  1796  19.45  1797  exdistrf  1864  19.9v  2011  exists1  2207  dfid3  4282  fsplit  6157  a9e2ndeq  27378  e2ebind  27382  a9e2ndeqVD  27735  e2ebindVD  27738  e2ebindALT  27756  a9e2ndeqALT  27758  bnj1131  27868  bnj1397  27916  bnj1189  28088
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator