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

Theorem rabssdv 3519
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 1196 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  x  e.  B ) ) )
32ralrimiv 2816 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  x  e.  B ) )
4 rabss 3516 . 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 974    e. wcel 1842   A.wral 2754   {crab 2758    C_ wss 3414
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rab 2763  df-in 3421  df-ss 3428
This theorem is referenced by:  suppss2OLD  6511  suppss2  6937  oemapvali  8135  cantnflem1  8140  cantnflem1OLD  8163  harval2  8410  zsupss  11216  ramub1lem1  14753  symggen  16819  efgsfo  17081  ablfacrp  17437  ablfac1eu  17444  pgpfac1lem5  17450  ablfaclem3  17458  nrmr0reg  20542  ptcmplem3  20846  abelthlem2  23119  lgamgulmlem1  23684  neibastop2lem  30588  topmeet  30592  cntotbnd  31574  mapdrvallem2  34665
  Copyright terms: Public domain W3C validator