Theorem r19.23ad 1742

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 1064	. 2 |- (ph -> (E.x(x e. A /\ ps) -> ch))
6		df-rex 1647	. 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 952   e. wcel 956  E.wex 978  E.wrex 1643

This theorem is referenced by:  r19.23adv 1743  uniiunlem 2128  reuuni4 2882  ralxfrd 2892  ralxfr 2894  onfr 2981  peano5 3148  ffnfv 3819  iunon 3900  iinon 3901  tz7.49 3950  oarec 4186  nneneq 4498  zorn2lem4 4771  zorn2lem5 4772  climsup 7099  caucvglem6 7106  atom1d 10217

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain