Theorem 19.23v 1295

Description: Special case of Theorem 19.23 of [Margaris] p. 90.

Assertion

Ref	Expression
19.23v	|- (A.x(ph -> ps) <-> (E.xph -> ps))

Distinct variable group:   ps,x

Proof of Theorem 19.23v

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 |- (ps -> A.xps)
2	1	19.23 1065	1 |- (A.x(ph -> ps) <-> (E.xph -> ps))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 956  E.wex 982

This theorem is referenced by:  19.23vv 1296  2eu4 1455  r19.23v 1744  r19.3rzv 2352  unissb 2532  dfiin2 2592  iunss 2595  dftr2 2687  ssrel 3253  cotr 3442  dffun2 3532  fununi 3569  f1fv 3880  aceq2 4741  ntreq0 7705  metcld 7964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983

Copyright terms: Public domain