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	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
	hbralrimi.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜓 ) )
Assertion	hbralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		hbralrimi.1	⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2		hbralrimi.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝜓 ) )
3	1 2	alrimih	⊢ ( 𝜑 → ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) )
4		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜓 ) )
5	3 4	sylibr	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝜓 )