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

Theorem ralrimiv 2445
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 1466 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2444 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    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  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  ralrimiva  2446  ralrimivw  2447  ralrimivv  2454  r19.27av  2504  rr19.3v  2755  rabssdv  3101  rzal  3379  trin  3946  class2seteq  3998  ralxfrALT  4289  ssorduni  4304  ordsucim  4317  onintonm  4334  issref  4814  funimaexglem  5097  resflem  5462  poxp  5997  rdgss  6148  dom2lem  6489  supisoti  6705  ordiso2  6728  updjud  6773  uzind  8857  zindd  8864  lbzbi  9101  icoshftf1o  9408  maxabslemval  10641  fisum0diag2  10841  alzdvds  11133  hashgcdeq  11482  bj-nntrans2  11847  bj-inf2vnlem1  11865
  Copyright terms: Public domain W3C validator