Theorem ralrimia 3234

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

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

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 2183

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

This theorem is referenced by:  funcnvmpt  6942  fompt  7063  vieta  33715  ss2iundf  43937  ismnushort  44579  modelaxreplem3  45258  ssrabdf  45396  ss2rabdf  45431  iunssdf  45437  rnmptssd  45477  dmmptdff  45504  axccd  45510  dmmptdf2  45514  rnmptbd2lem  45529  rnmptssdf  45535  rnmptbdlem  45536  ralrnmpt3  45540  rnmptssbi  45541  fconst7  45545  fmptdff  45552  rnmptssdff  45556  infleinf2  45695  unb2ltle  45696  uzublem  45711  cvgcaule  45772  climinf3  45997  limsupequzlem  46003  limsupre3uzlem  46016  climisp  46027  climrescn  46029  climxrrelem  46030  climxrre  46031  climxlim2lem  46126  dvnprodlem1  46227  saliunclf  46603  meaiuninc3v  46765  preimageiingt  47001  preimaleiinlt  47002  fsupdm  47123  finfdm  47127  iinfssc  49339  iinfsubc  49340