Theorem ralrimia 3231

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1784   ∈ wcel 2111  ∀wral 3047

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-12 2180

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785  df-ral 3048

This theorem is referenced by:  fompt  7051  ss2iundf  43751  ismnushort  44393  modelaxreplem3  45072  ssrabdf  45211  iunssdf  45252  rnmptssd  45292  dmmptdff  45319  axccd  45325  dmmptdf2  45329  rnmptbd2lem  45344  rnmptssdf  45350  rnmptbdlem  45351  ralrnmpt3  45355  rnmptssbi  45356  fconst7  45360  fmptdff  45367  rnmptssdff  45371  infleinf2  45511  unb2ltle  45512  uzublem  45527  cvgcaule  45588  climinf3  45813  limsupequzlem  45819  limsupre3uzlem  45832  climisp  45843  climrescn  45845  climxrrelem  45846  climxrre  45847  climxlim2lem  45942  dvnprodlem1  46043  saliunclf  46419  meaiuninc3v  46581  fsupdm  46939  finfdm  46943  iinfssc  49157  iinfsubc  49158