Theorem r19.23ad 1791

Description: Deduction from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).

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.2	. . 3 |- (ch -> A.xch)
3		r19.23ad.3	. . . 4 |- (ph -> (x e. A -> (ps -> ch)))
4	3	imp3a 359	. . 3 |- (ph -> ((x e. A /\ ps) -> ch))
5	1, 2, 4	19.23ad 1102	. 2 |- (ph -> (E.x(x e. A /\ ps) -> ch))
6		df-rex 1696	. 2 |- (E.x e. A ps <-> E.x(x e. A /\ ps))
7	5, 6	syl5ib 204	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 3   /\ wa 221  A.wal 990   e. wcel 994  E.wex 1016  E.wrex 1692

This theorem is referenced by:  r19.23adv 1792  uniiunlem 2184  onfr 3014  reuuni4 3110  ralxfrd 3120  ralxfr 3122  peano5 3241  ffnfv 3942  iunon 4207  iinon 4208  onopriun 4211  tz7.49 4260  oarec 4332  nneneq 4659  zorn2lem4 4937  zorn2lem5 4938  climsupi 7358  caucvglem6 7365  metequiv 8091  atom1d 10561  ordtypelem4 11430  ordtypelem7 11433  elomsubsd 11446  hscptsscld 11491  alexsublem3 11498  neibastop2lem1 11580  neibastop2lem3 11582  limfilcf 11683  indexa 11845  sdc 11877  totbndbnd 12000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011  ax-6o 1014

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-rex 1696

Copyright terms: Public domain