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

Theorem hbralrimi 2853
 Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). This theorem contains the common proof steps for ralrimi 2857 and ralrimiv 2869. 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 1642 . 2
4 df-ral 2812 . 2
53, 4sylibr 212 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  A.wal 1393  e.wcel 1818  A.wral 2807 This theorem is referenced by:  ralrimi  2857  ralrimiv  2869  bnj1145  34049 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631 This theorem depends on definitions:  df-bi 185  df-ral 2812
 Copyright terms: Public domain W3C validator