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

Theorem ss2rabdv 3543
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 2840 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3538 . 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 1869   A.wral 2776   {crab 2780    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rab 2785  df-in 3444  df-ss 3451
This theorem is referenced by:  sess1  4819  suppfnss  6949  suppssov1  6956  suppssfv  6960  harword  8084  mrcss  15515  ablfac1b  17696  mptscmfsupp0  18146  lspss  18200  aspss  18549  dsmmacl  19296  dsmmsubg  19298  dsmmlss  19299  scmatdmat  19532  clsss  20061  lfinpfin  20531  qustgpopn  21126  metss2lem  21518  equivcau  22262  rrxmvallem  22350  ovolsslem  22429  itg2monolem1  22700  lgamucov  23955  sqff1o  24101  musum  24112  cusgrafilem1  25199  suppss2fOLD  28233  locfinreflem  28669  omsmon  29128  omsmonOLD  29132  orvclteinc  29310  fin2solem  31889  poimirlem26  31924  poimirlem27  31925  cnambfre  31947  pclssN  33422  2polssN  33443  dihglblem3N  34826  dochss  34896  mapdordlem2  35168  nzss  36568  rmsuppss  39499  mndpsuppss  39500  scmsuppss  39501
  Copyright terms: Public domain W3C validator