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

Theorem ss2rabdv 3512
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 2804 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3507 . 2  |-  ( { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
42, 3sylibr 216 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    e. wcel 1889   A.wral 2739   {crab 2743    C_ wss 3406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-rab 2748  df-in 3413  df-ss 3420
This theorem is referenced by:  sess1  4805  suppfnss  6945  suppssov1  6952  suppssfv  6956  harword  8085  mrcss  15534  ablfac1b  17715  mptscmfsupp0  18165  lspss  18219  aspss  18568  dsmmacl  19316  dsmmsubg  19318  dsmmlss  19319  scmatdmat  19552  clsss  20081  lfinpfin  20551  qustgpopn  21146  metss2lem  21538  equivcau  22282  rrxmvallem  22370  ovolsslem  22449  itg2monolem1  22720  lgamucov  23975  sqff1o  24121  musum  24132  cusgrafilem1  25219  suppss2fOLD  28249  locfinreflem  28679  omsmon  29138  omsmonOLD  29142  orvclteinc  29320  fin2solem  31943  poimirlem26  31978  poimirlem27  31979  cnambfre  32001  pclssN  33471  2polssN  33492  dihglblem3N  34875  dochss  34945  mapdordlem2  35217  nzss  36677  cusgrfilem1  39526  rmsuppss  40259  mndpsuppss  40260  scmsuppss  40261
  Copyright terms: Public domain W3C validator