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

Syntax hints:   → wi 4   ∧ wa 399  Ⅎwnf 1805   ∈ wcel 2144  ∀wral 3078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-12 2214

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-nf 1806  df-ral 3079

This theorem is referenced by:  ralimdaa  3265  iineq2d  4975  funcnvmpt  6979  fompt  7101  rnmptssd  7107  vieta  33879  ss2iundf  44240  ismnushort  44882  modelaxreplem3  45561  ssrabdf  45698  ss2rabdf  45733  iunssdf  45739  dmmptdff  45804  axccd  45809  dmmptdf2  45813  rnmptbd2lem  45828  rnmptssdf  45834  rnmptbdlem  45835  ralrnmpt3  45839  rnmptssbi  45840  fconst7  45844  fmptdff  45851  rnmptssdff  45855  infleinf2  45993  unb2ltle  45994  uzublem  46009  cvgcaule  46070  climinf3  46295  limsupequzlem  46301  limsupre3uzlem  46314  climisp  46325  climrescn  46327  climxrrelem  46328  climxrre  46329  climxlim2lem  46424  dvnprodlem1  46525  fourierdlem113  46798  saliunclf  46901  meaiuninc3v  47063  preimageiingt  47299  preimaleiinlt  47300  fsupdm  47421  finfdm  47425  iinfssc  49683  iinfsubc  49684