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

Step	Hyp	Ref	Expression
1		19.9.1	. . 3
2	1	nfri 1874	. 2
3	2	19.9h 1891	1

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