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

Theorem ralrimivw 2459
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 2457 1  |-  ( ph  ->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1445   A.wral 2370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375
This theorem is referenced by:  exse  4187  sosng  4540  dmxpm  4687  exse2  4839  funco  5088  acexmidlemph  5683  mpt2eq12  5747  xpexgALT  5942  mpt2exg  6016  rdgtfr  6177  rdgruledefgg  6178  rdgivallem  6184  frecabex  6201  frectfr  6203  omfnex  6250  oeiv  6257  uniqs  6390  sbthlemi5  6750  sbthlemi6  6751  updjud  6853  exmidfodomrlemim  6924  genpdisj  7179  ltexprlemloc  7263  recexprlemloc  7287  cauappcvgprlemrnd  7306  cauappcvgprlemdisj  7307  caucvgprlemrnd  7329  caucvgprlemdisj  7330  caucvgprprlemrnd  7357  caucvgprprlemdisj  7358  recan  10657  climconst  10833  sumeq2ad  10912  dvdsext  11283  neif  11993  lmconst  12067  cndis  12092
  Copyright terms: Public domain W3C validator