Theorem 19.23v 1910

Description: Special case of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jun-1998.)

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		nfv 1673	. 2 |- F/ x ps
2	1	19.23 1843	1 |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1367   E.wex 1586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590

This theorem is referenced by:  19.23vv  1911  2mo2  2359  2eu4OLD  2369  euind  3145  reuind  3161  r19.3rzv  3772  unissb  4122  disjor  4275  dftr2  4386  ssrelrel  4939  cotr  5209  dffun2  5427  fununi  5483  dff13  5970  dffi2  7672  aceq2  8288  psgnunilem4  16002  metcld  20815  metcld2  20816  isch2  24625  disjorf  25922  funcnv5mpt  25987  dfon2lem8  27602  pm10.52  29615  truniALT  31246  tpid3gVD  31576  truniALTVD  31612  onfrALTVD  31625  unisnALT  31660  bnj1052  31964  bnj1030  31976