Theorem 19.23v 950

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(s):   ps,x

Proof of Theorem 19.23v

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

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672  E.wex 678

This theorem is referenced by:  19.23vv 951  2eu4 1070  r19.23v 1282  r19.3rzv 1767  unissb 1941  dfiin2 2015  iunss 2017  dftr2 2043  relss 2480  cotr 2625  dffun2 2674  fununi 2705  f1fv 2916  aceq2 3554

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org