Theorem ralrimia 3261

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  Ⅎwnf 1816   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-12 2213

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-ral 3077

This theorem is used by:  ralimdaa  3263  iineq2d  4974  funcnvmpt  6983  fompt  7106  rnmptssd  7112  vieta  34145  mh-inf3f1  37251  ss2iundf  44603  ismnushort  45229  modelaxreplem3  45907  ssrabdf  46051  ss2rabdf  46086  iunssdf  46092  dmmptdff  46157  axccd  46162  dmmptdf2  46166  rnmptbd2lem  46181  rnmptssdf  46187  rnmptbdlem  46188  ralrnmpt3  46192  rnmptssbi  46193  fconst7  46197  fmptdff  46204  rnmptssdff  46208  infleinf2  46346  unb2ltle  46347  uzublem  46362  cvgcaule  46423  climinf3  46648  limsupequzlem  46654  limsupre3uzlem  46667  climisp  46678  climrescn  46680  climxrrelem  46681  climxrre  46682  climxlim2lem  46777  dvnprodlem1  46878  fourierdlem113  47151  saliunclf  47254  meaiuninc3v  47416  preimageiingt  47652  preimaleiinlt  47653  fsupdm  47774  finfdm  47778  iinfssc  50087  iinfsubc  50088