Theorem ralrimia 3420

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788  df-ral 3068

This theorem is referenced by:  ralimda  3421  ismnushort  41808  rnmptssd  42624  dmmptdf  42652  axccd  42657  dmmptdf2  42665  mpteq12daOLD  42676  rnmptbd2lem  42683  rnmptssdf  42689  rnmptbdlem  42690  ralrnmpt3  42694  rnmptssbi  42696  fconst7  42701  infleinf2  42844  unb2ltle  42845  uzublem  42860  climinf3  43147  limsupequzlem  43153  limsupre3uzlem  43166  climisp  43177  climrescn  43179  climxrrelem  43180  climxrre  43181  climxlim2lem  43276  meaiuninc3v  43912