Theorem r19.21ai 1712

Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.)

Hypotheses

Ref	Expression
r19.21ai.1	|- (ph -> A.xph)
r19.21ai.2	|- (ph -> (x e. A -> ps))

Assertion

Ref	Expression
r19.21ai	|- (ph -> A.x e. A ps)

Proof of Theorem r19.21ai

Step	Hyp	Ref	Expression
1		r19.21ai.1	. . 3 |- (ph -> A.xph)
2		r19.21ai.2	. . 3 |- (ph -> (x e. A -> ps))
3	1, 2	19.21ai 998	. 2 |- (ph -> A.x(x e. A -> ps))
4		df-ral 1649	. 2 |- (A.x e. A ps <-> A.x(x e. A -> ps))
5	3, 4	sylibr 200	1 |- (ph -> A.x e. A ps)

Syntax hints:   -> wi 3  A.wal 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  r19.21aiv 1713  r19.22d 1735  r19.12 1740  zfrep6 3614  fnopabg 3615  rnssopab 3825  fopabco 3832  isotrALT 3898  tfr3 3926  mapxpen 4495  aceq6b 4742  ac6lem 4754  cmphmp 10521  cnfilca 10583  cnfilcaOLD 10584  cmpmon 10743

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

This theorem depends on definitions:  df-bi 147  df-ral 1649

Copyright terms: Public domain