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

Theorem ralrimi 2444
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 1460 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2364 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
53, 4sylibr 132 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287   F/wnf 1394    e. wcel 1438   A.wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  ralrimiv  2445  reximdai  2471  r19.12  2478  rexlimd  2486  rexlimd2  2487  r19.29af2  2508  r19.37  2519  ralidm  3378  iineq2d  3745  mpteq2da  3919  onintonm  4324  mpteqb  5377  fmptdf  5439  eusvobj2  5620  tfri3  6114  mapxpen  6544  fodjuomnilemdc  6778  fimaxre2  10622  zsupcllemstep  11023  bezoutlemmain  11069  bezoutlemzz  11073
  Copyright terms: Public domain W3C validator