Theorem r19.21ai 1715

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 1000	. 2 |- (ph -> A.x(x e. A -> ps))
4		df-ral 1652	. 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 956   e. wcel 960  A.wral 1648

This theorem is referenced by:  r19.21aiv 1716  r19.22d 1738  r19.12 1743  zfrep6 3620  fnopabg 3621  rnssopab 3831  fopabco 3838  isotrALT 3904  tfr3 3932  mapxpen 4501  aceq6b 4752  ac6lem 4764  cmphmp 10507  cnfilca 10562  cmpmon 10714

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

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

Copyright terms: Public domain