Theorem ralrimia 3264

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1781   ∈ wcel 2108  ∀wral 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-12 2178

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-nf 1782  df-ral 3068

This theorem is referenced by:  fompt  7152  ss2iundf  43621  ismnushort  44270  ssrabdf  45017  iunssdf  45061  rnmptssd  45103  dmmptdff  45130  axccd  45136  dmmptdf2  45140  mpteq12daOLD  45151  rnmptbd2lem  45157  rnmptssdf  45163  rnmptbdlem  45164  ralrnmpt3  45168  rnmptssbi  45170  fconst7  45174  fmptdff  45181  rnmptssdff  45185  infleinf2  45329  unb2ltle  45330  uzublem  45345  cvgcaule  45407  climinf3  45637  limsupequzlem  45643  limsupre3uzlem  45656  climisp  45667  climrescn  45669  climxrrelem  45670  climxrre  45671  climxlim2lem  45766  saliunclf  46243  meaiuninc3v  46405  fsupdm  46763  finfdm  46767