Theorem ralrimia 3234

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 3233	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  7072  ss2iundf  43642  ismnushort  44284  modelaxreplem3  44964  ssrabdf  45103  iunssdf  45144  rnmptssd  45184  dmmptdff  45211  axccd  45217  dmmptdf2  45221  rnmptbd2lem  45236  rnmptssdf  45242  rnmptbdlem  45243  ralrnmpt3  45247  rnmptssbi  45248  fconst7  45252  fmptdff  45259  rnmptssdff  45263  infleinf2  45404  unb2ltle  45405  uzublem  45420  cvgcaule  45481  climinf3  45708  limsupequzlem  45714  limsupre3uzlem  45727  climisp  45738  climrescn  45740  climxrrelem  45741  climxrre  45742  climxlim2lem  45837  dvnprodlem1  45938  saliunclf  46314  meaiuninc3v  46476  fsupdm  46834  finfdm  46838  iinfssc  49040  iinfsubc  49041