Theorem 19.23v 1807

Description: Version of 19.23 1966 with a dv condition instead of a non-freeness hypothesis. (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 1701	. . 3 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		19.9v 1801	. . 3 |- ( E. x ps <-> ps )
3	1, 2	syl6ib 229	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
4		ax-5 1748	. . . 4 |- ( ps -> A. x ps )
5	4	imim2i 16	. . 3 |- ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) )
6		19.38 1707	. . 3 |- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
7	5, 6	syl 17	. 2 |- ( ( E. x ph -> ps ) -> A. x ( ph -> ps ) )
8	3, 7	impbii 190	1 |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 187   A.wal 1435   E.wex 1659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794

This theorem depends on definitions:  df-bi 188  df-ex 1660

This theorem is referenced by:  19.23vv  1808  pm11.53v  1811  equsalvw  1836  2mo2  2346  euind  3258  reuind  3275  r19.3rzv  3890  unissb  4247  disjor  4405  dftr2  4517  ssrelrel  4950  cotrg  5226  dffun2  5607  fununi  5663  dff13  6170  dffi2  7939  aceq2  8550  psgnunilem4  17125  metcld  22261  metcld2  22262  isch2  26861  disjorf  28178  funcnv5mpt  28261  bnj1052  29779  bnj1030  29791  dfon2lem8  30430  elintima  36104  relexp0eq  36152  dfhe3  36227  pm10.52  36571  truniALT  36759  tpid3gVD  37098  truniALTVD  37135  onfrALTVD  37148  unisnALT  37183