Theorem 19.23v 1936

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		ax-17 1579	. 2 |- ( ps -> A. x ps )
2	1	19.23h 1551	1 |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   A.wal 1400   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-gen 1502  ax-ie2 1547  ax-17 1579

This theorem is used by:  19.23vv  1937  equsv  1938  2eu4  2180  gencbval  2871  euind  3013  reuind  3031  snssb  3848  unissb  3965  disjnim  4120  dftr2  4233  ssrelrel  4877  cotr  5172  dffun2  5390  fununi  5452  dff13  5977  acexmidlem2  6085