Theorem ralrimia 41767

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 416	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	1, 3	ralrimi 3180	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 399  Ⅎwnf 1785   ∈ wcel 2111  ∀wral 3106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2175

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3111

This theorem is referenced by:  ralimda  41774  rnmptssd  41824  rnmpt0  41849  dmmptdf  41854  axccd  41861  dmmptdf2  41869  mpteq12da  41879  rnmptbd2lem  41886  rnmptssdf  41892  rnmptbdlem  41893  ralrnmpt3  41897  rnmptssbi  41899  fconst7  41904  infleinf2  42051  unb2ltle  42052  uzublem  42067  climinf3  42358  limsupequzlem  42364  limsupre3uzlem  42377  climisp  42388  climrescn  42390  climxrrelem  42391  climxrre  42392  climxlim2lem  42487  meaiuninc3v  43123