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

Theorem ss2rabi 3268
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 3262 . 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 2626 1  |-  { x  e.  A  |  ph }  C_ 
{ x  e.  A  |  ps }
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   {crab 2560    C_ wss 3165
This theorem is referenced by:  supub  7226  suplub  7227  card2on  7284  rankval4  7555  fin1a2lem12  8053  catlid  13601  catrid  13602  gsumval2  14476  lbsextlem3  15929  psrbagsn  16252  musum  20447  ppiub  20459  itgaddnclem2  25010  usisuslgra  28247  lclkrs2  32352
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rab 2565  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator