Theorem r19.23ad 1737

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 361	. . 3 |- (ph -> ((x e. A /\ ps) -> ch))
5	1, 2, 4	19.23ad 1062	. 2 |- (ph -> (E.x(x e. A /\ ps) -> ch))
6		df-rex 1642	. 2 |- (E.x e. A ps <-> E.x(x e. A /\ ps))
7	5, 6	syl5ib 206	1 |- (ph -> (E.x e. A ps -> ch))

Syntax hints:   -> wi 3   /\ wa 223  A.wal 951   e. wcel 955  E.wex 977  E.wrex 1638

This theorem is referenced by:  r19.23adv 1738  uniiunlem 2122  reuuni4 2877  ralxfrd 2887  ralxfr 2889  onfr 2976  peano5 3143  ffnfv 3813  iunon 3894  iinon 3895  tz7.49 3944  oarec 4180  nneneq 4492  zorn2lem4 4763  zorn2lem5 4764  climsup 7091  caucvglem6 7098  atom1d 10188

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain