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

Theorem 19.9 1893
Description: A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. See 19.9v 1754 for a version requiring fewer axioms. (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
Assertion
Ref Expression
19.9

Proof of Theorem 19.9
StepHypRef Expression
1 19.9.1 . . 3
21nfri 1874 . 2
3219.9h 1891 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  E.wex 1612  F/wnf 1616
This theorem is referenced by:  exlimd  1914  19.19  1959  19.36  1964  19.44  1969  19.45  1970  19.41  1971  exists1  2388  dfid3  4801  fsplit  6905  ax6e2ndeq  33332  e2ebind  33336  ax6e2ndeqVD  33709  e2ebindVD  33712  e2ebindALT  33729  ax6e2ndeqALT  33731  bnj1189  34065  bj-exexbiex  34254  bj-exalbial  34256
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
  Copyright terms: Public domain W3C validator