Theorem hbralrimi

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

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

Proof

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