ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralrimi Unicode version

Theorem ralrimi 2478
Description: Inference from Theorem 19.21 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 10-Oct-1999.)
Hypotheses
Ref Expression
ralrimi.1  |-  F/ x ph
ralrimi.2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
Assertion
Ref Expression
ralrimi  |-  ( ph  ->  A. x  e.  A  ps )

Proof of Theorem ralrimi
StepHypRef Expression
1 ralrimi.1 . . 3  |-  F/ x ph
2 ralrimi.2 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2alrimi 1485 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2396 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
53, 4sylibr 133 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312   F/wnf 1419    e. wcel 1463   A.wral 2391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2396
This theorem is referenced by:  ralrimiv  2479  reximdai  2505  r19.12  2513  rexlimd  2521  rexlimd2  2522  r19.29af2  2547  r19.37  2558  ralidm  3431  iineq2d  3801  mpteq2da  3985  onintonm  4401  mpteqb  5477  fmptdf  5543  eusvobj2  5726  tfri3  6230  mapxpen  6708  fodjuomnilemdc  6982  fimaxre2  10949  zsupcllemstep  11545  bezoutlemmain  11593  bezoutlemzz  11597  exmidunben  11845  mulcncf  12666  limccnp2lem  12720
  Copyright terms: Public domain W3C validator