MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2rabi Unicode version

Theorem ss2rabi 3255
Description: Inference of restricted abstraction subclass from implication. (Contributed by NM, 14-Oct-1999.)
Hypothesis
Ref Expression
ss2rabi.1  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
ss2rabi  |-  { x  e.  A  |  ph }  C_ 
{ x  e.  A  |  ps }

Proof of Theorem ss2rabi
StepHypRef Expression
1 ss2rab 3249 . 2  |-  ( { x  e.  A  |  ph }  C_  { x  e.  A  |  ps } 
<-> 
A. x  e.  A  ( ph  ->  ps )
)
2 ss2rabi.1 . 2  |-  ( x  e.  A  ->  ( ph  ->  ps ) )
31, 2mprgbir 2613 1  |-  { x  e.  A  |  ph }  C_ 
{ x  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   {crab 2547    C_ wss 3152
This theorem is referenced by:  supub  7210  suplub  7211  card2on  7268  rankval4  7539  fin1a2lem12  8037  catlid  13585  catrid  13586  gsumval2  14460  lbsextlem3  15913  psrbagsn  16236  musum  20431  ppiub  20443  usisuslgra  28113  lclkrs2  31730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rab 2552  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator