Theorem hbralrimi 2954

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 2957 and ralrimiv 2965. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.)

Hypotheses

Ref	Expression
hbralrimi.1	|- ( ph -> A. x ph )
hbralrimi.2	|- ( ph -> ( x e. A -> ps ) )

Assertion

Ref	Expression
hbralrimi	|- ( ph -> A. x e. A ps )

Proof of Theorem hbralrimi

Step	Hyp	Ref	Expression
1		hbralrimi.1	. . 3 |- ( ph -> A. x ph )
2		hbralrimi.2	. . 3 |- ( ph -> ( x e. A -> ps ) )
3	1, 2	alrimih 1751	. 2 |- ( ph -> A. x ( x e. A -> ps ) )
4		df-ral 2917	. 2 |- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
5	3, 4	sylibr 224	1 |- ( ph -> A. x e. A ps )

Syntax hints:   -> wi 4   A.wal 1481   e. wcel 1990   A.wral 2912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  ralrimi  2957  ralrimiv  2965  bnj1145  31061