Theorem ralrimia 3263

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2215

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3079

This theorem is used by:  ralimdaa  3265  iineq2d  4978  funcnvmpt  6992  fompt  7114  rnmptssd  7120  vieta  34077  ss2iundf  44486  ismnushort  45112  modelaxreplem3  45790  ssrabdf  45934  ss2rabdf  45969  iunssdf  45975  dmmptdff  46040  axccd  46045  dmmptdf2  46049  rnmptbd2lem  46064  rnmptssdf  46070  rnmptbdlem  46071  ralrnmpt3  46075  rnmptssbi  46076  fconst7  46080  fmptdff  46087  rnmptssdff  46091  infleinf2  46229  unb2ltle  46230  uzublem  46245  cvgcaule  46306  climinf3  46531  limsupequzlem  46537  limsupre3uzlem  46550  climisp  46561  climrescn  46563  climxrrelem  46564  climxrre  46565  climxlim2lem  46660  dvnprodlem1  46761  fourierdlem113  47034  saliunclf  47137  meaiuninc3v  47299  preimageiingt  47535  preimaleiinlt  47536  fsupdm  47657  finfdm  47661  iinfssc  49970  iinfsubc  49971