Theorem ralrimia 3228

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

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

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 2008  ax-12 2178

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

This theorem is referenced by:  fompt  7052  ss2iundf  43652  ismnushort  44294  modelaxreplem3  44974  ssrabdf  45113  iunssdf  45154  rnmptssd  45194  dmmptdff  45221  axccd  45227  dmmptdf2  45231  rnmptbd2lem  45246  rnmptssdf  45252  rnmptbdlem  45253  ralrnmpt3  45257  rnmptssbi  45258  fconst7  45262  fmptdff  45269  rnmptssdff  45273  infleinf2  45413  unb2ltle  45414  uzublem  45429  cvgcaule  45490  climinf3  45717  limsupequzlem  45723  limsupre3uzlem  45736  climisp  45747  climrescn  45749  climxrrelem  45750  climxrre  45751  climxlim2lem  45846  dvnprodlem1  45947  saliunclf  46323  meaiuninc3v  46485  fsupdm  46843  finfdm  46847  iinfssc  49062  iinfsubc  49063