Theorem 19.37v 1769

Description: Version of 19.37 1967 with a dv condition, requiring fewer axioms. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
19.37v	|- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) )

Distinct variable group:   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem 19.37v

Step	Hyp	Ref	Expression
1		19.35 1688	. 2 |- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
2		19.3v 1756	. . 3 |- ( A. x ph <-> ph )
3	2	imbi1i 325	. 2 |- ( ( A. x ph -> E. x ps ) <-> ( ph -> E. x ps ) )
4	1, 3	bitri 249	1 |- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1393   E.wex 1613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748

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

This theorem is referenced by:  19.37iv  1770  axrep5  4573  fvn0ssdmfun  6023  kmlem14  8560  kmlem15  8561  eqvincg  27501  19.37vv  31494  pm11.61  31503  rmoanim  32387  relopabVD  33844  bnj132  33922  bnj1098  33985  bnj150  34077  bnj865  34124  bnj996  34156  bnj1021  34165  bnj1090  34178  bnj1176  34204  bj-axrep5  34521