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

Theorem ss2rabdv 3519
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 2817 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3514 . 2  |-  ( { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } 
<-> 
A. x  e.  A  ( ps  ->  ch )
)
42, 3sylibr 212 1  |-  ( ph  ->  { x  e.  A  |  ps }  C_  { x  e.  A  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1842   A.wral 2753   {crab 2757    C_ wss 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-rab 2762  df-in 3420  df-ss 3427
This theorem is referenced by:  sess1  4790  suppssfvOLD  6511  suppssov1OLD  6512  suppfnss  6927  suppssov1  6934  suppssfv  6938  harword  8024  mrcss  15228  ablfac1b  17439  mptscmfsupp0  17894  lspss  17948  aspss  18299  dsmmacl  19068  dsmmsubg  19070  dsmmlss  19071  scmatdmat  19307  clsss  19845  lfinpfin  20315  qustgpopn  20908  metss2lem  21304  equivcau  22029  rrxmvallem  22121  ovolsslem  22185  itg2monolem1  22447  lgamucov  23691  sqff1o  23835  musum  23846  cusgrafilem1  24883  suppss2f  27906  locfinreflem  28282  omsmon  28732  orvclteinc  28906  fin2solem  31391  cnambfre  31415  pclssN  32891  2polssN  32912  dihglblem3N  34295  dochss  34365  mapdordlem2  34637  nzss  36050  rmsuppss  38455  mndpsuppss  38456  scmsuppss  38457
  Copyright terms: Public domain W3C validator