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

Theorem ralrimi 2528
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 1502 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  ps ) )
4 df-ral 2440 . 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 1333   F/wnf 1440    e. wcel 2128   A.wral 2435
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 1427  ax-gen 1429  ax-4 1490
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440
This theorem is referenced by:  ralrimiv  2529  reximdai  2555  r19.12  2563  rexlimd  2571  rexlimd2  2572  r19.29af2  2597  r19.37  2609  ralidm  3495  iineq2d  3871  mpteq2da  4055  onintonm  4478  mpteqb  5560  fmptdf  5626  eusvobj2  5812  tfri3  6316  mapxpen  6795  fodjuomnilemdc  7089  cc3  7190  fimaxre2  11137  fprodcllemf  11521  fprodap0f  11544  fprodle  11548  zsupcllemstep  11844  bezoutlemmain  11897  bezoutlemzz  11901  exmidunben  12225  mulcncf  13061  limccnp2lem  13115
  Copyright terms: Public domain W3C validator