Theorem ralrimia 3237

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-12 2185

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786  df-ral 3053

This theorem is referenced by:  ralimdaa  3239  iineq2d  4958  funcnvmpt  6945  fompt  7066  rnmptssd  7072  vieta  33743  ss2iundf  44110  ismnushort  44752  modelaxreplem3  45431  ssrabdf  45569  ss2rabdf  45604  iunssdf  45610  dmmptdff  45676  axccd  45682  dmmptdf2  45686  rnmptbd2lem  45701  rnmptssdf  45707  rnmptbdlem  45708  ralrnmpt3  45712  rnmptssbi  45713  fconst7  45717  fmptdff  45724  rnmptssdff  45728  infleinf2  45866  unb2ltle  45867  uzublem  45882  cvgcaule  45943  climinf3  46168  limsupequzlem  46174  limsupre3uzlem  46187  climisp  46198  climrescn  46200  climxrrelem  46201  climxrre  46202  climxlim2lem  46297  dvnprodlem1  46398  saliunclf  46774  meaiuninc3v  46936  preimageiingt  47172  preimaleiinlt  47173  fsupdm  47294  finfdm  47298  iinfssc  49550  iinfsubc  49551