Theorem ralrimia 3258

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

Syntax hints:   → wi 4   ∧ wa 395  Ⅎwnf 1783   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-12 2177

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784  df-ral 3062

This theorem is referenced by:  fompt  7138  ss2iundf  43672  ismnushort  44320  modelaxreplem3  44997  ssrabdf  45120  iunssdf  45161  rnmptssd  45201  dmmptdff  45228  axccd  45234  dmmptdf2  45238  mpteq12daOLD  45249  rnmptbd2lem  45255  rnmptssdf  45261  rnmptbdlem  45262  ralrnmpt3  45266  rnmptssbi  45267  fconst7  45271  fmptdff  45278  rnmptssdff  45282  infleinf2  45425  unb2ltle  45426  uzublem  45441  cvgcaule  45502  climinf3  45731  limsupequzlem  45737  limsupre3uzlem  45750  climisp  45761  climrescn  45763  climxrrelem  45764  climxrre  45765  climxlim2lem  45860  dvnprodlem1  45961  saliunclf  46337  meaiuninc3v  46499  fsupdm  46857  finfdm  46861