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 39835
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 397 . 2 (𝜑 → (𝑥𝐴𝜓))
41, 3ralrimi 3106 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wnf 1856  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-nf 1858  df-ral 3066
This theorem is referenced by:  ralimda  39846  funimaeq  39976  ralrnmpt3  39989  rnmptssbi  39992  fconst7  39999  infleinf2  40154  unb2ltle  40155  uzublem  40170  climinf3  40463  limsupequzlem  40469  limsupre3uzlem  40482  climisp  40493  climrescn  40495  climxrrelem  40496  climxrre  40497  climxlim2lem  40586  meaiuninc3v  41215
  Copyright terms: Public domain W3C validator