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

Theorem ralrimiv 2434
Description: Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Nov-1994.)
Hypothesis
Ref Expression
ralrimiv.1  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
Assertion
Ref Expression
ralrimiv  |-  ( ph  ->  A. x  e.  A  ps )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem ralrimiv
StepHypRef Expression
1 nfv 1462 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2433 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1434   A.wral 2349
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-ral 2354
This theorem is referenced by:  ralrimiva  2435  ralrimivw  2436  ralrimivv  2443  r19.27av  2493  rr19.3v  2734  rabssdv  3075  rzal  3346  trin  3893  class2seteq  3945  ralxfrALT  4225  ssorduni  4239  ordsucim  4252  onintonm  4269  issref  4737  funimaexglem  5013  poxp  5884  rdgss  6032  dom2lem  6319  supisoti  6482  ordiso2  6505  uzind  8539  zindd  8546  lbzbi  8782  icoshftf1o  9089  maxabslemval  10232  alzdvds  10399  bj-nntrans2  10905  bj-inf2vnlem1  10923
  Copyright terms: Public domain W3C validator