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

Theorem ss2rabdv 3574
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 2871 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3569 . 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 369    e. wcel 1762   A.wral 2807   {crab 2811    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rab 2816  df-in 3476  df-ss 3483
This theorem is referenced by:  reusv6OLD  4651  sess1  4840  suppssfvOLD  6506  suppssov1OLD  6507  suppfnss  6915  suppssov1  6922  suppssfv  6926  harword  7980  mrcss  14860  ablfac1b  16904  mptscmfsupp0  17352  lspss  17406  aspss  17745  dsmmacl  18532  dsmmsubg  18534  dsmmlss  18535  scmatdmat  18777  clsss  19314  divstgpopn  20346  metss2lem  20742  equivcau  21467  rrxmvallem  21559  ovolsslem  21623  itg2monolem1  21885  sqff1o  23177  musum  23188  cusgrafilem1  24141  suppss2f  27136  omsmon  27893  orvclteinc  28040  lgamucov  28206  fin2solem  29602  cnambfre  29627  lfinpfin  29762  rmsuppss  31911  mndpsuppss  31912  scmsuppss  31913  pclssN  34565  2polssN  34586  dihglblem3N  35967  dochss  36037  mapdordlem2  36309
  Copyright terms: Public domain W3C validator