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

Theorem rabssdv 3580
Description: Subclass of a restricted class abstraction (deduction rule). (Contributed by NM, 2-Feb-2015.)
Hypothesis
Ref Expression
rabssdv.1  |-  ( (
ph  /\  x  e.  A  /\  ps )  ->  x  e.  B )
Assertion
Ref Expression
rabssdv  |-  ( ph  ->  { x  e.  A  |  ps }  C_  B
)
Distinct variable groups:    x, B    ph, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rabssdv
StepHypRef Expression
1 rabssdv.1 . . . 4  |-  ( (
ph  /\  x  e.  A  /\  ps )  ->  x  e.  B )
213exp 1195 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  x  e.  B ) ) )
32ralrimiv 2876 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  x  e.  B ) )
4 rabss 3577 . 2  |-  ( { x  e.  A  |  ps }  C_  B  <->  A. x  e.  A  ( ps  ->  x  e.  B ) )
53, 4sylibr 212 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973    e. wcel 1767   A.wral 2814   {crab 2818    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rab 2823  df-in 3483  df-ss 3490
This theorem is referenced by:  suppss2OLD  6514  suppss2  6934  oemapvali  8103  cantnflem1  8108  cantnflem1OLD  8131  harval2  8378  zsupss  11171  ramub1lem1  14403  symggen  16301  efgsfo  16563  ablfacrp  16919  ablfac1eu  16926  pgpfac1lem5  16932  ablfaclem3  16940  nrmr0reg  20013  ptcmplem3  20317  abelthlem2  22589  lgamgulmlem1  28239  neibastop2lem  29809  topmeet  29813  cntotbnd  29923  mapdrvallem2  36460
  Copyright terms: Public domain W3C validator