Theorem 19.23v 1293

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

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954  E.wex 980

This theorem is referenced by:  19.23vv 1294  2eu4 1452  r19.23v 1741  r19.3rzv 2348  unissb 2528  dfiin2 2588  iunss 2591  dftr2 2682  ssrel 3247  cotr 3436  dffun2 3526  fununi 3563  f1fv 3874  aceq2 4731  ntreq0 7708  metcld 7967

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

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

Copyright terms: Public domain