Theorem hbralrimi 2853

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 2857 and ralrimiv 2869. 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
hbralrimi.2

Assertion

Ref	Expression
hbralrimi

Proof of Theorem hbralrimi

Step	Hyp	Ref	Expression
1		hbralrimi.1	. . 3
2		hbralrimi.2	. . 3
3	1, 2	alrimih 1642	. 2
4		df-ral 2812	. 2
5	3, 4	sylibr 212	1

Syntax hints:  ->wi 4  A.wal 1393  e.wcel 1818  A.wral 2807

This theorem is referenced by:  ralrimi  2857  ralrimiv  2869  bnj1145  34049

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

This theorem depends on definitions:  df-bi 185  df-ral 2812