Theorem ralrimia 3240

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

Syntax hints:   → wi 4   ∧ wa 397  Ⅎwnf 1791   ∈ wcel 2121  ∀wral 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-12 2191

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-nf 1792  df-ral 3056

This theorem is referenced by:  ralimdaa  3242  iineq2d  4948  funcnvmpt  6941  fompt  7063  rnmptssd  7069  vieta  33776  ss2iundf  44118  ismnushort  44760  modelaxreplem3  45439  ssrabdf  45576  ss2rabdf  45611  iunssdf  45617  dmmptdff  45682  axccd  45687  dmmptdf2  45691  rnmptbd2lem  45706  rnmptssdf  45712  rnmptbdlem  45713  ralrnmpt3  45717  rnmptssbi  45718  fconst7  45722  fmptdff  45729  rnmptssdff  45733  infleinf2  45871  unb2ltle  45872  uzublem  45887  cvgcaule  45948  climinf3  46173  limsupequzlem  46179  limsupre3uzlem  46192  climisp  46203  climrescn  46205  climxrrelem  46206  climxrre  46207  climxlim2lem  46302  dvnprodlem1  46403  saliunclf  46779  meaiuninc3v  46941  preimageiingt  47177  preimaleiinlt  47178  fsupdm  47299  finfdm  47303  iinfssc  49561  iinfsubc  49562