Theorem ralrimia 3241

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

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

This theorem is referenced by:  fompt  7108  ss2iundf  43683  ismnushort  44325  modelaxreplem3  45005  ssrabdf  45139  iunssdf  45180  rnmptssd  45220  dmmptdff  45247  axccd  45253  dmmptdf2  45257  rnmptbd2lem  45272  rnmptssdf  45278  rnmptbdlem  45279  ralrnmpt3  45283  rnmptssbi  45284  fconst7  45288  fmptdff  45295  rnmptssdff  45299  infleinf2  45441  unb2ltle  45442  uzublem  45457  cvgcaule  45518  climinf3  45745  limsupequzlem  45751  limsupre3uzlem  45764  climisp  45775  climrescn  45777  climxrrelem  45778  climxrre  45779  climxlim2lem  45874  dvnprodlem1  45975  saliunclf  46351  meaiuninc3v  46513  fsupdm  46871  finfdm  46875  iinfssc  49024  iinfsubc  49025