Theorem 19.9v 1754

Description: Version of 19.9 1893 with a dv condition, requiring fewer axioms. Any formula can be existentially quantified using a variable which it does not contain. See also 19.3v 1755. (Contributed by NM, 28-May-1995.) Remove dependency on ax-7 1790. (Revised by Wolf Lammen, 4-Dec-2017.)

Assertion

Ref	Expression
19.9v

Distinct variable group:   ,

Proof of Theorem 19.9v

Step	Hyp	Ref	Expression
1		ax5e 1706	. 2
2		19.8v 1753	. 2
3	1, 2	impbii 188	1

Syntax hints:  <->wb 184  E.wex 1612

This theorem is referenced by:  19.3v  1755  19.23v  1760  19.36v  1762  19.44v  1770  19.41v  1771  zfcndpow  9015  volfiniune  28202  prter2  30622  rfcnnnub  31411  relopabVD  33701  bnj937  33830  bnj594  33970  bnj907  34023  bnj1128  34046  bnj1145  34049

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

This theorem depends on definitions:  df-bi 185  df-ex 1613