Theorem 19.23v 1288

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 968	. 2 |- (ps -> A.xps)
2	1	19.23 1059	1 |- (A.x(ph -> ps) <-> (E.xph -> ps))

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951  E.wex 977

This theorem is referenced by:  19.23vv 1289  2eu4 1445  r19.23v 1733  r19.3rzv 2338  unissb 2518  dfiin2 2578  iunss 2581  dftr2 2672  ssrel 3237  cotr 3420  dffun2 3512  fununi 3549  f1fv 3859  aceq2 4703  ntreq0 7650  metcld 7901

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

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

Copyright terms: Public domain