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

Theorem ralrimia 41274
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 413 . 2 (𝜑 → (𝑥𝐴𝜓))
41, 3ralrimi 3213 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wnf 1775  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776  df-ral 3140
This theorem is referenced by:  ralimda  41282  rnmptssd  41334  rnmpt0  41359  dmmptdf  41364  axccd  41371  dmmptdf2  41379  mpteq12da  41389  rnmptbd2lem  41396  rnmptssdf  41402  rnmptbdlem  41403  ralrnmpt3  41407  rnmptssbi  41410  fconst7  41415  infleinf2  41564  unb2ltle  41565  uzublem  41580  climinf3  41873  limsupequzlem  41879  limsupre3uzlem  41892  climisp  41903  climrescn  41905  climxrrelem  41906  climxrre  41907  climxlim2lem  42002  meaiuninc3v  42643
  Copyright terms: Public domain W3C validator