Theorem r19.23ad 1745

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 1066	. 2 |- (ph -> (E.x(x e. A /\ ps) -> ch))
6		df-rex 1650	. 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 954   e. wcel 958  E.wex 980  E.wrex 1646

This theorem is referenced by:  r19.23adv 1746  uniiunlem 2132  reuuni4 2887  ralxfrd 2897  ralxfr 2899  onfr 2986  peano5 3153  ffnfv 3828  iunon 3909  iinon 3910  tz7.49 3959  oarec 4196  nneneq 4512  zorn2lem4 4791  zorn2lem5 4792  climsup 7155  caucvglem6 7162  atom1d 10280

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain