This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to \forall x φ$
	hbralrimi.2	$⊢ φ \to (x \in A \to ψ)$
Assertion	hbralrimi	$⊢ φ \to \forall x \in A ψ$

Proof

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