Theorem ralrimia 3234

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

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

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 2008  ax-12 2178

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

This theorem is referenced by:  fompt  7072  ss2iundf  43641  ismnushort  44283  modelaxreplem3  44963  ssrabdf  45102  iunssdf  45143  rnmptssd  45183  dmmptdff  45210  axccd  45216  dmmptdf2  45220  rnmptbd2lem  45235  rnmptssdf  45241  rnmptbdlem  45242  ralrnmpt3  45246  rnmptssbi  45247  fconst7  45251  fmptdff  45258  rnmptssdff  45262  infleinf2  45403  unb2ltle  45404  uzublem  45419  cvgcaule  45480  climinf3  45707  limsupequzlem  45713  limsupre3uzlem  45726  climisp  45737  climrescn  45739  climxrrelem  45740  climxrre  45741  climxlim2lem  45836  dvnprodlem1  45937  saliunclf  46313  meaiuninc3v  46475  fsupdm  46833  finfdm  46837  iinfssc  49039  iinfsubc  49040