Theorem ralrimia 3256

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

Syntax hints:   → wi 4   ∧ wa 397  Ⅎwnf 1786   ∈ wcel 2107  ∀wral 3062

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 1914  ax-6 1972  ax-7 2012  ax-12 2172

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

This theorem is referenced by:  ss2iundf  42410  ismnushort  43060  ssrabdf  43804  iunssdf  43850  rnmptssd  43895  dmmptdff  43922  axccd  43928  dmmptdf2  43935  mpteq12daOLD  43946  rnmptbd2lem  43952  rnmptssdf  43958  rnmptbdlem  43959  ralrnmpt3  43963  rnmptssbi  43965  fconst7  43969  fmptdff  43976  rnmptssdff  43980  infleinf2  44124  unb2ltle  44125  uzublem  44140  cvgcaule  44202  climinf3  44432  limsupequzlem  44438  limsupre3uzlem  44451  climisp  44462  climrescn  44464  climxrrelem  44465  climxrre  44466  climxlim2lem  44561  saliunclf  45038  meaiuninc3v  45200  fsupdm  45558  finfdm  45562