Theorem 19.23v 1932

Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020.)

Assertion

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

Distinct variable group:   ps, x

Allowed substitution hint:   ph( x)

Proof of Theorem 19.23v

Step	Hyp	Ref	Expression
1		exim 1633	. . 3 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		19.9v 1728	. . 3 |- ( E. x ps <-> ps )
3	1, 2	syl6ib 226	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
4		ax-5 1680	. . . 4 |- ( ps -> A. x ps )
5	4	imim2i 14	. . 3 |- ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) )
6		19.38 1639	. . 3 |- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
7	5, 6	syl 16	. 2 |- ( ( E. x ph -> ps ) -> A. x ( ph -> ps ) )
8	3, 7	impbii 188	1 |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1377   E.wex 1596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719

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

This theorem is referenced by:  19.23vv  1934  2mo2  2381  2eu4OLD  2391  euind  3295  reuind  3312  r19.3rzv  3926  unissb  4282  disjor  4436  dftr2  4547  ssrelrel  5108  cotrg  5383  dffun2  5603  fununi  5659  dff13  6164  dffi2  7893  aceq2  8510  psgnunilem4  16372  metcld  21589  metcld2  21590  isch2  25932  disjorf  27231  funcnv5mpt  27302  dfon2lem8  29117  pm10.52  31140  truniALT  32685  tpid3gVD  33015  truniALTVD  33051  onfrALTVD  33064  unisnALT  33099  bnj1052  33403  bnj1030  33415