Theorem 19.23v 1902

Description: Version of 19.23 2080 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 1761	. . 3 |- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2		19.9v 1896	. . 3 |- ( E. x ps <-> ps )
3	1, 2	syl6ib 241	. 2 |- ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
4		ax-5 1839	. . . 4 |- ( ps -> A. x ps )
5	4	imim2i 16	. . 3 |- ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) )
6		19.38 1766	. . 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 199	1 |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  19.23vv  1903  pm11.53v  1906  equsalvw  1931  2mo2  2550  euind  3393  reuind  3411  unissb  4469  disjor  4634  dftr2  4754  ssrelrel  5220  cotrg  5507  dffun2  5898  fununi  5964  dff13  6512  dffi2  8329  aceq2  8942  psgnunilem4  17917  metcld  23104  metcld2  23105  isch2  28080  disjorf  29392  funcnv5mpt  29469  bnj1052  31043  bnj1030  31055  dfon2lem8  31695  bj-ssbeq  32627  bj-ssb0  32628  bj-ssb1a  32632  bj-ssb1  32633  bj-ssbequ2  32643  bj-ssbid2ALT  32646  ineleq  34119  elmapintrab  37882  elinintrab  37883  undmrnresiss  37910  elintima  37945  relexp0eq  37993  dfhe3  38069  pm10.52  38564  truniALT  38751  tpid3gVD  39077  truniALTVD  39114  onfrALTVD  39127  unisnALT  39162