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

Theorem 19.9 1832
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 1813 . 2  |-  ( ph  ->  A. x ph )
3219.9h 1830 1  |-  ( E. x ph  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   E.wex 1587   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  exlimd  1852  19.19  1897  19.36  1904  19.44  1909  19.45  1910  19.41  1911  exists1  2385  dfid3  4746  fsplit  6788  cnvoprab  26175  ax6e2ndeq  31601  e2ebind  31605  ax6e2ndeqVD  31978  e2ebindVD  31981  e2ebindALT  31998  ax6e2ndeqALT  32000  bnj1189  32333  bj-exexbiex  32523  bj-exalbial  32525
  Copyright terms: Public domain W3C validator