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

Theorem ss2rabi 3543
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 3537 . 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 2786 1  |-  { x  e.  A  |  ph }  C_ 
{ x  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   {crab 2775    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rab 2780  df-in 3443  df-ss 3450
This theorem is referenced by:  supub  7983  suplub  7984  card2on  8079  rankval4  8347  fin1a2lem12  8849  catlid  15589  catrid  15590  gsumval2  16523  lbsextlem3  18383  psrbagsn  18718  musum  24119  ppiub  24131  usisuslgra  25091  disjxwwlks  25463  clwlknclwlkdifnum  25688  omssubadd  29137  omssubaddOLD  29141  bj-unrab  31499  poimirlem26  31931  poimirlem27  31932  lclkrs2  35078  umgrupgr  39024  usgruspgr  39080
  Copyright terms: Public domain W3C validator