Theorem ralrimia 3270

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

Syntax hints:   → wi 4   ∧ wa 400  Ⅎwnf 1810   ∈ wcel 2149  ∀wral 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811  df-ral 3086

This theorem is referenced by:  ralimdaa  3272  iineq2d  4982  funcnvmpt  6992  fompt  7114  rnmptssd  7120  vieta  33915  ss2iundf  44312  ismnushort  44938  modelaxreplem3  45616  ssrabdf  45760  ss2rabdf  45795  iunssdf  45801  dmmptdff  45866  axccd  45871  dmmptdf2  45875  rnmptbd2lem  45890  rnmptssdf  45896  rnmptbdlem  45897  ralrnmpt3  45901  rnmptssbi  45902  fconst7  45906  fmptdff  45913  rnmptssdff  45917  infleinf2  46055  unb2ltle  46056  uzublem  46071  cvgcaule  46132  climinf3  46357  limsupequzlem  46363  limsupre3uzlem  46376  climisp  46387  climrescn  46389  climxrrelem  46390  climxrre  46391  climxlim2lem  46486  dvnprodlem1  46587  fourierdlem113  46860  saliunclf  46963  meaiuninc3v  47125  preimageiingt  47361  preimaleiinlt  47362  fsupdm  47483  finfdm  47487  iinfssc  49755  iinfsubc  49756