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

Theorem ralrimi 2561
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 1533 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2473 . 2  |-  ( A. x  e.  A  ps  <->  A. x ( x  e.  A  ->  ps )
)
53, 4sylibr 134 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1362   F/wnf 1471    e. wcel 2160   A.wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473
This theorem is referenced by:  ralrimiv  2562  reximdai  2588  r19.12  2596  rexlimd  2604  rexlimd2  2605  r19.29af2  2630  r19.37  2642  ralidm  3538  iineq2d  3921  mpteq2da  4107  onintonm  4534  mpteqb  5626  fmptdf  5693  eusvobj2  5881  tfri3  6391  mapxpen  6875  fodjuomnilemdc  7171  cc3  7296  fimaxre2  11266  fprodcllemf  11652  fprodap0f  11675  fprodle  11679  zsupcllemstep  11977  bezoutlemmain  12030  bezoutlemzz  12034  exmidunben  12476  mulcncf  14543  limccnp2lem  14597
  Copyright terms: Public domain W3C validator