Theorem hbralrimi 3101

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3141 and ralrimiv 3102. 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 1826	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
4		df-ral 3069	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜓))
5	3, 4	sylibr 233	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2106  ∀wral 3064

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

This theorem depends on definitions:  df-bi 206  df-ral 3069

This theorem is referenced by:  ralrimiv  3102  ralrimi  3141  bnj1145  32973