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

Theorem ss2rabdv 3542
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 2830 . 2  |-  ( ph  ->  A. x  e.  A  ( ps  ->  ch )
)
3 ss2rab 3537 . 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 1758   A.wral 2799   {crab 2803    C_ wss 3437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-rab 2808  df-in 3444  df-ss 3451
This theorem is referenced by:  reusv6OLD  4612  sess1  4797  suppssfvOLD  6427  suppssov1OLD  6428  suppfnss  6825  suppssov1  6832  suppssfv  6836  harword  7892  mrcss  14674  ablfac1b  16694  mptscmfsupp0  17135  lspss  17189  aspss  17527  dsmmacl  18292  dsmmsubg  18294  dsmmlss  18295  clsss  18791  divstgpopn  19823  metss2lem  20219  equivcau  20944  rrxmvallem  21036  ovolsslem  21100  itg2monolem1  21362  sqff1o  22654  musum  22665  cusgrafilem1  23540  suppss2f  26106  omsmon  26856  orvclteinc  27003  lgamucov  27169  fin2solem  28564  cnambfre  28589  lfinpfin  28724  rmsuppss  30932  mndpsuppss  30933  scmsuppss  30934  scmatdmat  31063  pclssN  33877  2polssN  33898  dihglblem3N  35279  dochss  35349  mapdordlem2  35621
  Copyright terms: Public domain W3C validator