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

Theorem ss2rabdv 3340
Description: Deduction of restricted abstraction subclass from implication. (Contributed by NM, 30-May-2006.)
Hypothesis
Ref Expression
ss2rabdv.1  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
ss2rabdv  |-  ( ph  ->  { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem ss2rabdv
StepHypRef Expression
1 ss2rabdv.1 . . 3  |-  ( (
ph  /\  x  e.  A )  ->  ( ps  ->  ch ) )
21ralrimiva 2711 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3335 . 2  |-  ( { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
42, 3sylibr 203 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1715   A.wral 2628   {crab 2632    C_ wss 3238
This theorem is referenced by:  sess1  4464  reusv6OLD  4648  suppssfv  6201  suppssov1  6202  harword  7426  mrcss  13728  ablfac1b  15515  lspss  15951  aspss  16282  clsss  17008  divstgpopn  18015  metss2lem  18270  equivcau  18941  ovolsslem  19058  itg2monolem1  19320  sqff1o  20643  musum  20654  suppss2f  23452  orvclteinc  24181  lgamucov  24270  lfinpfin  25810  dsmmacl  26713  dsmmsubg  26715  dsmmlss  26716  pclssN  30154  2polssN  30175  dihglblem3N  31556  dochss  31626  mapdordlem2  31898
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ral 2633  df-rab 2637  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator