Theorem ralrimia 3237

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

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

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 3046

This theorem is referenced by:  fompt  7093  ss2iundf  43655  ismnushort  44297  modelaxreplem3  44977  ssrabdf  45116  iunssdf  45157  rnmptssd  45197  dmmptdff  45224  axccd  45230  dmmptdf2  45234  rnmptbd2lem  45249  rnmptssdf  45255  rnmptbdlem  45256  ralrnmpt3  45260  rnmptssbi  45261  fconst7  45265  fmptdff  45272  rnmptssdff  45276  infleinf2  45417  unb2ltle  45418  uzublem  45433  cvgcaule  45494  climinf3  45721  limsupequzlem  45727  limsupre3uzlem  45740  climisp  45751  climrescn  45753  climxrrelem  45754  climxrre  45755  climxlim2lem  45850  dvnprodlem1  45951  saliunclf  46327  meaiuninc3v  46489  fsupdm  46847  finfdm  46851  iinfssc  49050  iinfsubc  49051