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