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 40060
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 402 . 2 (𝜑 → (𝑥𝐴𝜓))
41, 3ralrimi 3136 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  wnf 1879  wcel 2157  wral 3087
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-12 2213
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-nf 1880  df-ral 3092
This theorem is referenced by:  ralimda  40071  funimaeq  40196  ralrnmpt3  40209  rnmptssbi  40212  fconst7  40219  infleinf2  40372  unb2ltle  40373  uzublem  40388  climinf3  40680  limsupequzlem  40686  limsupre3uzlem  40699  climisp  40710  climrescn  40712  climxrrelem  40713  climxrre  40714  climxlim2lem  40803  meaiuninc3v  41432
  Copyright terms: Public domain W3C validator