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

Theorem ss2rabdv 3496
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 2809 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3491 . 2  |-  ( { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
42, 3sylibr 217 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    e. wcel 1904   A.wral 2756   {crab 2760    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-rab 2765  df-in 3397  df-ss 3404
This theorem is referenced by:  sess1  4807  suppfnss  6959  suppssov1  6966  suppssfv  6970  harword  8098  mrcss  15600  ablfac1b  17781  mptscmfsupp0  18231  lspss  18285  aspss  18633  dsmmacl  19381  dsmmsubg  19383  dsmmlss  19384  scmatdmat  19617  clsss  20146  lfinpfin  20616  qustgpopn  21212  metss2lem  21604  equivcau  22348  rrxmvallem  22436  ovolsslem  22515  itg2monolem1  22787  lgamucov  24042  sqff1o  24188  musum  24199  cusgrafilem1  25286  suppss2fOLD  28313  locfinreflem  28741  omsmon  29199  omsmonOLD  29203  orvclteinc  29381  fin2solem  31995  poimirlem26  32030  poimirlem27  32031  cnambfre  32053  pclssN  33530  2polssN  33551  dihglblem3N  34934  dochss  35004  mapdordlem2  35276  nzss  36736  cusgrfilem1  39681  rmsuppss  40663  mndpsuppss  40664  scmsuppss  40665
  Copyright terms: Public domain W3C validator