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 2353  unissb 2533  dfiin2 2593  iunss 2596  dftr2 2688  ssrel 3254  cotr 3443  dffun2 3533  fununi 3570  f1fv 3881  aceq2 4748  ntreq0 7712  metcld 7971

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