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

Theorem ralrimiv 2529
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 1508 . 2  |-  F/ x ph
2 ralrimiv.1 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
31, 2ralrimi 2528 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    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  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440
This theorem is referenced by:  ralrimiva  2530  ralrimivw  2531  ralrimivv  2538  r19.27av  2592  rr19.3v  2851  rabssdv  3208  rzal  3491  trin  4072  class2seteq  4124  ralxfrALT  4427  ssorduni  4446  ordsucim  4459  onintonm  4476  issref  4968  funimaexglem  5253  resflem  5631  poxp  6179  rdgss  6330  dom2lem  6717  supisoti  6954  ordiso2  6979  updjud  7026  uzind  9275  zindd  9282  lbzbi  9525  icoshftf1o  9895  maxabslemval  11108  xrmaxiflemval  11147  fisum0diag2  11344  alzdvds  11746  hashgcdeq  12114  tgcl  12475  distop  12496  neiuni  12572  cnpnei  12630  isxmetd  12758  fsumcncntop  12967  bj-nntrans2  13538  bj-inf2vnlem1  13556
  Copyright terms: Public domain W3C validator