Theorem ralrimia 3261

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  Ⅎwnf 1815   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816  df-ral 3077

This theorem is used by:  ralimdaa  3263  iineq2d  4974  funcnvmpt  6995  fompt  7118  rnmptssd  7124  vieta  34212  mh-inf3f1  37329  ss2iundf  44659  ismnushort  45285  modelaxreplem3  45970  ssrabdf  46130  ss2rabdf  46165  iunssdf  46171  dmmptdff  46236  axccd  46241  dmmptdf2  46245  rnmptbd2lem  46260  rnmptssdf  46266  rnmptbdlem  46267  ralrnmpt3  46271  rnmptssbi  46272  fconst7  46276  fmptdff  46283  rnmptssdff  46287  infleinf2  46424  unb2ltle  46425  uzublem  46440  cvgcaule  46501  climinf3  46726  limsupequzlem  46732  limsupre3uzlem  46745  climisp  46756  climrescn  46758  climxrrelem  46759  climxrre  46760  climxlim2lem  46855  dvnprodlem1  46956  fourierdlem113  47229  saliunclf  47332  meaiuninc3v  47494  preimageiingt  47730  preimaleiinlt  47731  fsupdm  47852  finfdm  47856  iinfssc  50165  iinfsubc  50166