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

Theorem ralrimi 2541
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 1515 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2453 . 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 1346   F/wnf 1453    e. wcel 2141   A.wral 2448
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 1440  ax-gen 1442  ax-4 1503
This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453
This theorem is referenced by:  ralrimiv  2542  reximdai  2568  r19.12  2576  rexlimd  2584  rexlimd2  2585  r19.29af2  2610  r19.37  2622  ralidm  3515  iineq2d  3893  mpteq2da  4078  onintonm  4501  mpteqb  5586  fmptdf  5653  eusvobj2  5839  tfri3  6346  mapxpen  6826  fodjuomnilemdc  7120  cc3  7230  fimaxre2  11190  fprodcllemf  11576  fprodap0f  11599  fprodle  11603  zsupcllemstep  11900  bezoutlemmain  11953  bezoutlemzz  11957  exmidunben  12381  mulcncf  13385  limccnp2lem  13439
  Copyright terms: Public domain W3C validator