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

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

Proof of Theorem ralrimivw
StepHypRef Expression
1 ralrimivw.1 . . 3  |-  ( ph  ->  ps )
21a1d 22 . 2  |-  ( ph  ->  ( x  e.  A  ->  ps ) )
32ralrimiv 2434 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:  exse  4099  sosng  4439  dmxpm  4583  exse2  4729  funco  4970  acexmidlemph  5536  mpt2eq12  5596  xpexgALT  5791  mpt2exg  5865  rdgtfr  6023  rdgruledefgg  6024  rdgivallem  6030  frecabex  6047  frectfr  6049  omfnex  6093  oeiv  6100  uniqs  6230  genpdisj  6775  ltexprlemloc  6859  recexprlemloc  6883  cauappcvgprlemrnd  6902  cauappcvgprlemdisj  6903  caucvgprlemrnd  6925  caucvgprlemdisj  6926  caucvgprprlemrnd  6953  caucvgprprlemdisj  6954  recan  10133  climconst  10267  dvdsext  10400
  Copyright terms: Public domain W3C validator