Theorem 19.23v 1672

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

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296  E.wex 1326

This theorem is referenced by:  19.23vv 1673  2eu4 1856  euind 2439  reuind 2450  r19.3rzv 2962  tpid3g 3115  unissb 3208  dfiin2OLD 3288  iunssOLD 3292  dftr2 3413  ssrelOLD 4076  ssrelrel 4083  ssrelrelOLD 4084  cotr 4302  cotrOLD 4303  dffun2 4431  fununi 4481  dff13 4850  truniALT 5845  aceq2 5893  ntreq0 8984  metcld 9245  dfon2lem8 13856  prtlem18 16279  pm10.52 16312  tpid3gVD 16666  truniALTVD 16702

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327

Copyright terms: Public domain