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	$$⊢\phi \to \forall x\phi$$
	hbralrimi.2	$$⊢\phi \to \left(x\in A\to \psi \right)$$
Assertion	hbralrimi	$$⊢\phi \to \forall x\in A\psi$$

Proof

Step	Hyp	Ref	Expression
1		hbralrimi.1	$$⊢\phi \to \forall x\phi$$
2		hbralrimi.2	$$⊢\phi \to \left(x\in A\to \psi \right)$$
3	1 2	alrimih	$$⊢\phi \to \forall x\left(x\in A\to \psi \right)$$
4		df-ral	$$⊢\forall x\in A\psi \leftrightarrow \forall x\left(x\in A\to \psi \right)$$
5	3 4	sylibr	$$⊢\phi \to \forall x\in A\psi$$