Theorem 19.23v 1829

Description: Version of 19.23 2004 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 1717	. . 3 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		19.9v 1823	. . 3 |- ( E. x ps <-> ps )
3	1, 2	syl6ib 234	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
4		ax-5 1769	. . . 4 |- ( ps -> A. x ps )
5	4	imim2i 16	. . 3 |- ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) )
6		19.38 1723	. . 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 192	1 |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1453   E.wex 1674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816

This theorem depends on definitions:  df-bi 190  df-ex 1675

This theorem is referenced by:  19.23vv  1830  pm11.53v  1833  equsalvw  1858  2mo2  2390  euind  3237  reuind  3255  r19.3rzv  3874  unissb  4243  disjor  4401  dftr2  4513  ssrelrel  4954  cotrg  5230  dffun2  5611  fununi  5671  dff13  6184  dffi2  7963  aceq2  8576  psgnunilem4  17187  metcld  22324  metcld2  22325  isch2  26925  disjorf  28238  funcnv5mpt  28321  bnj1052  29833  bnj1030  29845  dfon2lem8  30485  bj-ssbeq  31285  bj-ssb0  31286  bj-ssb1a  31290  bj-ssb1  31291  bj-ssbequ2  31301  bj-ssbid2ALT  31304  elmapintrab  36227  elinintrab  36228  undmrnresiss  36255  elintima  36290  relexp0eq  36338  dfhe3  36415  pm10.52  36758  truniALT  36946  tpid3gVD  37278  truniALTVD  37315  onfrALTVD  37328  unisnALT  37363