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

Theorem rabssdv 3479
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 1204 . . 3  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  x  e.  B ) ) )
32ralrimiv 2772 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  x  e.  B ) )
4 rabss 3476 . 2  |-  ( { x  e.  A  |  ps }  C_  B  <->  A. x  e.  A  ( ps  ->  x  e.  B ) )
53, 4sylibr 215 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982    e. wcel 1872   A.wral 2709   {crab 2713    C_ wss 3374
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 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ral 2714  df-rab 2718  df-in 3381  df-ss 3388
This theorem is referenced by:  suppss2  6899  oemapvali  8136  cantnflem1  8141  harval2  8378  zsupss  11199  ramub1lem1  14922  symggen  17049  efgsfo  17327  ablfacrp  17637  ablfac1eu  17644  pgpfac1lem5  17650  ablfaclem3  17658  nrmr0reg  20701  ptcmplem3  21006  abelthlem2  23324  lgamgulmlem1  23891  neibastop2lem  30960  topmeet  30964  cntotbnd  32035  mapdrvallem2  35125
  Copyright terms: Public domain W3C validator