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

Syntax hints:   → wi 4   ∧ wa 396  Ⅎwnf 1785   ∈ wcel 2106  ∀wral 3061

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 1913  ax-6 1971  ax-7 2011  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786  df-ral 3062

This theorem is referenced by:  fompt  7119  ss2iundf  42492  ismnushort  43142  ssrabdf  43886  iunssdf  43932  rnmptssd  43974  dmmptdff  44001  axccd  44007  dmmptdf2  44014  mpteq12daOLD  44025  rnmptbd2lem  44031  rnmptssdf  44037  rnmptbdlem  44038  ralrnmpt3  44042  rnmptssbi  44044  fconst7  44048  fmptdff  44055  rnmptssdff  44059  infleinf2  44203  unb2ltle  44204  uzublem  44219  cvgcaule  44281  climinf3  44511  limsupequzlem  44517  limsupre3uzlem  44530  climisp  44541  climrescn  44543  climxrrelem  44544  climxrre  44545  climxlim2lem  44640  saliunclf  45117  meaiuninc3v  45279  fsupdm  45637  finfdm  45641