Theorem ralrimia 41405

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

Syntax hints:   → wi 4   ∧ wa 398  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-12 2177

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785  df-ral 3145

This theorem is referenced by:  ralimda  41413  rnmptssd  41465  rnmpt0  41490  dmmptdf  41495  axccd  41502  dmmptdf2  41510  mpteq12da  41520  rnmptbd2lem  41527  rnmptssdf  41533  rnmptbdlem  41534  ralrnmpt3  41538  rnmptssbi  41541  fconst7  41546  infleinf2  41695  unb2ltle  41696  uzublem  41711  climinf3  42004  limsupequzlem  42010  limsupre3uzlem  42023  climisp  42034  climrescn  42036  climxrrelem  42037  climxrre  42038  climxlim2lem  42133  meaiuninc3v  42773