Theorem r19.23ad 2213

Description: Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (The proof was shortened by Andrew Salmon, 30-May-2011.)

Hypotheses

Ref	Expression
r19.23ad.1	|- (ph -> A.xph)
r19.23ad.2	|- (ch -> A.xch)
r19.23ad.3	|- (ph -> (x e. A -> (ps -> ch)))

Assertion

Ref	Expression
r19.23ad	|- (ph -> (E.x e. A ps -> ch))

Proof of Theorem r19.23ad

Step	Hyp	Ref	Expression
1		r19.23ad.1	. . 3 |- (ph -> A.xph)
2		r19.23ad.3	. . 3 |- (ph -> (x e. A -> (ps -> ch)))
3	1, 2	r19.21ai 2174	. 2 |- (ph -> A.x e. A (ps -> ch))
4		r19.23ad.2	. . 3 |- (ch -> A.xch)
5	4	r19.23 2206	. 2 |- (A.x e. A (ps -> ch) <-> (E.x e. A ps -> ch))
6	3, 5	sylib 215	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 3  A.wal 1296   e. wcel 1300  A.wral 2105  E.wrex 2106

This theorem is referenced by:  r19.23adv 2215  uniiunlem 2693  onfr 3702  reuuni4 3813  ralxfrd 3837  ralxfr 3839  peano5 3975  ffnfv 4801  iunon 5114  iinon 5115  onopriun 5118  tz7.49 5168  oarec 5244  nneneq 5606  ordtypelem4 5687  ordtypelem7 5690  elomsubsd 5885  zorn2lem4 5953  zorn2lem5 5954  climsupi 8415  caucvglem6 8422  metequiv 9158  atom1d 11925  lbzbi 13657  ordtypelem4OLD 15378  ordtypelem7OLD 15381  elomsubsdOLD 15394  hscptsscld 15434  alexsublem3 15439  neibastop2lem1 15519  neibastop2lem3 15521  limfilcf 15587  indexa 15753  sdc 15811  totbndbnd 15944  glbconx 17029

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

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain