Theorem ralrimia 3430

Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypotheses

Ref	Expression
ralrimia.1	⊢ Ⅎ𝑥𝜑
ralrimia.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)

Assertion

Ref	Expression
ralrimia	⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralrimia

Step	Hyp	Ref	Expression
1		ralrimia.1	. 2 ⊢ Ⅎ𝑥𝜑
2		ralrimia.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝜓)
3	2	ex 413	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	1, 3	ralrimi 3141	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 396  Ⅎwnf 1786   ∈ 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  ax-5 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787  df-ral 3069

This theorem is referenced by:  ralimda  3431  ismnushort  41919  rnmptssd  42735  dmmptdf  42763  axccd  42768  dmmptdf2  42776  mpteq12daOLD  42787  rnmptbd2lem  42794  rnmptssdf  42800  rnmptbdlem  42801  ralrnmpt3  42805  rnmptssbi  42807  fconst7  42812  infleinf2  42954  unb2ltle  42955  uzublem  42970  climinf3  43257  limsupequzlem  43263  limsupre3uzlem  43276  climisp  43287  climrescn  43289  climxrrelem  43290  climxrre  43291  climxlim2lem  43386  meaiuninc3v  44022