Theorem ralrimia 3255

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 3254	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1779   ∈ wcel 2105  ∀wral 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-12 2174

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-nf 1780  df-ral 3059

This theorem is referenced by:  fompt  7137  ss2iundf  43648  ismnushort  44296  modelaxreplem3  44944  ssrabdf  45054  iunssdf  45098  rnmptssd  45138  dmmptdff  45165  axccd  45171  dmmptdf2  45175  mpteq12daOLD  45186  rnmptbd2lem  45192  rnmptssdf  45198  rnmptbdlem  45199  ralrnmpt3  45203  rnmptssbi  45205  fconst7  45209  fmptdff  45216  rnmptssdff  45220  infleinf2  45363  unb2ltle  45364  uzublem  45379  cvgcaule  45441  climinf3  45671  limsupequzlem  45677  limsupre3uzlem  45690  climisp  45701  climrescn  45703  climxrrelem  45704  climxrre  45705  climxlim2lem  45800  dvnprodlem1  45901  saliunclf  46277  meaiuninc3v  46439  fsupdm  46797  finfdm  46801