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

Theorem ralrimiv 2479
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 1491 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2478 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1463   A.wral 2391
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 1406  ax-gen 1408  ax-4 1470  ax-17 1489
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2396
This theorem is referenced by:  ralrimiva  2480  ralrimivw  2481  ralrimivv  2488  r19.27av  2542  rr19.3v  2795  rabssdv  3145  rzal  3428  trin  4004  class2seteq  4055  ralxfrALT  4356  ssorduni  4371  ordsucim  4384  onintonm  4401  issref  4889  funimaexglem  5174  resflem  5550  poxp  6095  rdgss  6246  dom2lem  6632  supisoti  6863  ordiso2  6886  updjud  6933  uzind  9113  zindd  9120  lbzbi  9357  icoshftf1o  9714  maxabslemval  10920  xrmaxiflemval  10959  fisum0diag2  11156  alzdvds  11448  hashgcdeq  11799  tgcl  12128  distop  12149  neiuni  12225  cnpnei  12283  isxmetd  12411  fsumcncntop  12620  bj-nntrans2  12952  bj-inf2vnlem1  12970
  Copyright terms: Public domain W3C validator