Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ralrimia Structured version   Visualization version   GIF version

Theorem ralrimia 41605
 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
StepHypRef Expression
1 ralrimia.1 . 2 𝑥𝜑
2 ralrimia.2 . . 3 ((𝜑𝑥𝐴) → 𝜓)
32ex 416 . 2 (𝜑 → (𝑥𝐴𝜓))
41, 3ralrimi 3210 1 (𝜑 → ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  Ⅎwnf 1785   ∈ wcel 2115  ∀wral 3132 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-12 2179 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-nf 1786  df-ral 3137 This theorem is referenced by:  ralimda  41613  rnmptssd  41665  rnmpt0  41690  dmmptdf  41695  axccd  41702  dmmptdf2  41710  mpteq12da  41720  rnmptbd2lem  41727  rnmptssdf  41733  rnmptbdlem  41734  ralrnmpt3  41738  rnmptssbi  41741  fconst7  41746  infleinf2  41893  unb2ltle  41894  uzublem  41909  climinf3  42200  limsupequzlem  42206  limsupre3uzlem  42219  climisp  42230  climrescn  42232  climxrrelem  42233  climxrre  42234  climxlim2lem  42329  meaiuninc3v  42965
 Copyright terms: Public domain W3C validator