Theorem ralrimia 3263

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400  Ⅎwnf 1812   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-12 2212

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-nf 1813  df-ral 3079

This theorem is used by:  ralimdaa  3265  iineq2d  4979  funcnvmpt  6991  fompt  7113  rnmptssd  7119  vieta  33979  ss2iundf  44413  ismnushort  45039  modelaxreplem3  45717  ssrabdf  45861  ss2rabdf  45896  iunssdf  45902  dmmptdff  45967  axccd  45972  dmmptdf2  45976  rnmptbd2lem  45991  rnmptssdf  45997  rnmptbdlem  45998  ralrnmpt3  46002  rnmptssbi  46003  fconst7  46007  fmptdff  46014  rnmptssdff  46018  infleinf2  46156  unb2ltle  46157  uzublem  46172  cvgcaule  46233  climinf3  46458  limsupequzlem  46464  limsupre3uzlem  46477  climisp  46488  climrescn  46490  climxrrelem  46491  climxrre  46492  climxlim2lem  46587  dvnprodlem1  46688  fourierdlem113  46961  saliunclf  47064  meaiuninc3v  47226  preimageiingt  47462  preimaleiinlt  47463  fsupdm  47584  finfdm  47588  iinfssc  49863  iinfsubc  49864