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 39836
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  39847  funimaeq  39979  ralrnmpt3  39992  rnmptssbi  39995  fconst7  40002  infleinf2  40157  unb2ltle  40158  uzublem  40173  climinf3  40466  limsupequzlem  40472  limsupre3uzlem  40485  climisp  40496  climrescn  40498  climxrrelem  40499  climxrre  40500  climxlim2lem  40589  meaiuninc3v  41218
  Copyright terms: Public domain W3C validator