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

Theorem rabssdv 3432
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 1186 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  x  e.  B ) ) )
32ralrimiv 2798 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  x  e.  B ) )
4 rabss 3429 . 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 965    e. wcel 1756   A.wral 2715   {crab 2719    C_ wss 3328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ral 2720  df-rab 2724  df-in 3335  df-ss 3342
This theorem is referenced by:  suppss2OLD  6315  suppss2  6723  oemapvali  7892  cantnflem1  7897  cantnflem1OLD  7920  harval2  8167  zsupss  10944  ramub1lem1  14087  symggen  15976  efgsfo  16236  ablfacrp  16567  ablfac1eu  16574  pgpfac1lem5  16580  ablfaclem3  16588  nrmr0reg  19322  ptcmplem3  19626  abelthlem2  21897  lgamgulmlem1  27015  neibastop2lem  28581  topmeet  28585  cntotbnd  28695  mapdrvallem2  35290
  Copyright terms: Public domain W3C validator