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

Theorem ss2rabdv 3392
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 2757 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3387 . 2  |-  ( { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
42, 3sylibr 204 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   A.wral 2674   {crab 2678    C_ wss 3288
This theorem is referenced by:  sess1  4518  reusv6OLD  4701  suppssfv  6268  suppssov1  6269  harword  7497  mrcss  13804  ablfac1b  15591  lspss  16023  aspss  16354  clsss  17081  divstgpopn  18110  metss2lem  18502  equivcau  19214  ovolsslem  19341  itg2monolem1  19603  sqff1o  20926  musum  20937  cusgrafilem1  21449  suppss2f  24010  orvclteinc  24694  lgamucov  24783  cnambfre  26162  lfinpfin  26281  dsmmacl  27083  dsmmsubg  27085  dsmmlss  27086  pclssN  30388  2polssN  30409  dihglblem3N  31790  dochss  31860  mapdordlem2  32132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ral 2679  df-rab 2683  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator