Theorem ralrimia 3428

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1789   ∈ wcel 2109  ∀wral 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-12 2174

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-nf 1790  df-ral 3070

This theorem is referenced by:  ralimda  3429  ismnushort  41872  rnmptssd  42688  dmmptdf  42716  axccd  42721  dmmptdf2  42729  mpteq12daOLD  42740  rnmptbd2lem  42747  rnmptssdf  42753  rnmptbdlem  42754  ralrnmpt3  42758  rnmptssbi  42760  fconst7  42765  infleinf2  42908  unb2ltle  42909  uzublem  42924  climinf3  43211  limsupequzlem  43217  limsupre3uzlem  43230  climisp  43241  climrescn  43243  climxrrelem  43244  climxrre  43245  climxlim2lem  43340  meaiuninc3v  43976