Theorem ralrimia 3245

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 411	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝜓))
4	1, 3	ralrimi 3244	1 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ∧ wa 394  Ⅎwnf 1777   ∈ wcel 2098  ∀wral 3050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-nf 1778  df-ral 3051

This theorem is referenced by:  fompt  7131  ss2iundf  43263  ismnushort  43912  ssrabdf  44653  iunssdf  44698  rnmptssd  44740  dmmptdff  44767  axccd  44773  dmmptdf2  44777  mpteq12daOLD  44788  rnmptbd2lem  44794  rnmptssdf  44800  rnmptbdlem  44801  ralrnmpt3  44805  rnmptssbi  44807  fconst7  44811  fmptdff  44818  rnmptssdff  44822  infleinf2  44966  unb2ltle  44967  uzublem  44982  cvgcaule  45044  climinf3  45274  limsupequzlem  45280  limsupre3uzlem  45293  climisp  45304  climrescn  45306  climxrrelem  45307  climxrre  45308  climxlim2lem  45403  saliunclf  45880  meaiuninc3v  46042  fsupdm  46400  finfdm  46404