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  6943  fompt  7064  rnmptssd  7070  vieta  33739  ss2iundf  44104  ismnushort  44746  modelaxreplem3  45425  ssrabdf  45563  ss2rabdf  45598  iunssdf  45604  dmmptdff  45670  axccd  45676  dmmptdf2  45680  rnmptbd2lem  45695  rnmptssdf  45701  rnmptbdlem  45702  ralrnmpt3  45706  rnmptssbi  45707  fconst7  45711  fmptdff  45718  rnmptssdff  45722  infleinf2  45860  unb2ltle  45861  uzublem  45876  cvgcaule  45937  climinf3  46162  limsupequzlem  46168  limsupre3uzlem  46181  climisp  46192  climrescn  46194  climxrrelem  46195  climxrre  46196  climxlim2lem  46291  dvnprodlem1  46392  saliunclf  46768  meaiuninc3v  46930  preimageiingt  47166  preimaleiinlt  47167  fsupdm  47288  finfdm  47292  iinfssc  49544  iinfsubc  49545