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

Theorem ralrimivw 2506
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 2504 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1480   A.wral 2416
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421
This theorem is referenced by:  r19.27v  2559  r19.28v  2560  exse  4258  sosng  4612  dmxpm  4759  exse2  4913  funco  5163  acexmidlemph  5767  mpoeq12  5831  xpexgALT  6031  mpoexg  6109  rdgtfr  6271  rdgruledefgg  6272  rdgivallem  6278  frecabex  6295  frectfr  6297  omfnex  6345  oeiv  6352  uniqs  6487  sbthlemi5  6849  sbthlemi6  6850  updjud  6967  exmidfodomrlemim  7057  exmidaclem  7064  cc4f  7084  genpdisj  7338  ltexprlemloc  7422  recexprlemloc  7446  cauappcvgprlemrnd  7465  cauappcvgprlemdisj  7466  caucvgprlemrnd  7488  caucvgprlemdisj  7489  caucvgprprlemrnd  7516  caucvgprprlemdisj  7517  suplocexpr  7540  recan  10888  climconst  11066  sumeq2ad  11145  dvdsext  11560  neif  12320  lmconst  12395  cndis  12420
  Copyright terms: Public domain W3C validator