MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hbralrimi Structured version   Visualization version   GIF version

Theorem hbralrimi 3138
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 3239 and ralrimiv 3139. Its main advantage over these two is its minimal references to axioms. The proof is extracted from NM's previous work. (Contributed by Wolf Lammen, 4-Dec-2019.)
Hypotheses
Ref Expression
hbralrimi.1 (𝜑 → ∀𝑥𝜑)
hbralrimi.2 (𝜑 → (𝑥𝐴𝜓))
Assertion
Ref Expression
hbralrimi (𝜑 → ∀𝑥𝐴 𝜓)

Proof of Theorem hbralrimi
StepHypRef Expression
1 hbralrimi.1 . . 3 (𝜑 → ∀𝑥𝜑)
2 hbralrimi.2 . . 3 (𝜑 → (𝑥𝐴𝜓))
31, 2alrimih 1827 . 2 (𝜑 → ∀𝑥(𝑥𝐴𝜓))
4 df-ral 3062 . 2 (∀𝑥𝐴 𝜓 ↔ ∀𝑥(𝑥𝐴𝜓))
53, 4sylibr 233 1 (𝜑 → ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wcel 2107  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ral 3062
This theorem is referenced by:  ralrimiv  3139  ralrimi  3239  bnj1145  33662
  Copyright terms: Public domain W3C validator