ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssrdv Unicode version

Theorem ssrdv 2978
Description: Deduction rule based on subclass definition. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
ssrdv.1  |-  ( ph  ->  ( x  e.  A  ->  x  e.  B ) )
Assertion
Ref Expression
ssrdv  |-  ( ph  ->  A  C_  B )
Distinct variable groups:    x, A    x, B    ph, x

Proof of Theorem ssrdv
StepHypRef Expression
1 ssrdv.1 . . 3  |-  ( ph  ->  ( x  e.  A  ->  x  e.  B ) )
21alrimiv 1770 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 2961 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 141 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1257    e. wcel 1409    C_ wss 2944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2951  df-ss 2958
This theorem is referenced by:  sscon  3104  ssdif  3105  unss1  3139  ssrin  3189  eq0rdv  3288  uniss  3628  intss1  3657  intmin  3662  intssunim  3664  iunss1  3695  iinss1  3696  ss2iun  3699  ssiun  3726  ssiun2  3727  iinss  3735  iinss2  3736  trintssmOLD  3898  sspwb  3979  tron  4146  ssorduni  4240  ordsson  4245  ordpwsucss  4318  xpsspw  4477  relop  4513  dmss  4561  dmcosseq  4630  ssrnres  4790  chfnrn  5305  ffnfv  5350  f1imass  5440  fo1stresm  5815  fo2ndresm  5816  fo2ndf  5875  reldmtpos  5898  smoiun  5946  tfrlemi14d  5977  nndifsnid  6110  qsss  6195  fidifsnid  6362  onunsnss  6385  addnqprlemrl  6712  addnqprlemru  6713  addnqprlemfl  6714  addnqprlemfu  6715  mulnqprlemrl  6728  mulnqprlemru  6729  mulnqprlemfl  6730  mulnqprlemfu  6731  distrlem1prl  6737  distrlem1pru  6738  distrlem5prl  6741  distrlem5pru  6742  ltprordil  6744  ltexprlemfl  6764  ltexprlemrl  6765  ltexprlemfu  6766  ltexprlemru  6767  addcanprleml  6769  addcanprlemu  6770  recexprlem1ssl  6788  recexprlem1ssu  6789  recexprlemss1l  6790  recexprlemss1u  6791  aptiprleml  6794  aptiprlemu  6795  cauappcvgprlemladdfu  6809  cauappcvgprlemladdfl  6810  cauappcvgprlemladdru  6811  cauappcvgprlemladdrl  6812  caucvgprlemladdfu  6832  caucvgprlemladdrl  6833  peano5uzti  8404  uzss  8588  ixxdisj  8872  ixxss1  8873  ixxss2  8874  ixxss12  8875  iocssre  8922  icossre  8923  iccssre  8924  icodisj  8960  fzss1  9027  fzss2  9028  fzoss1  9128  fzosplit  9134  fzouzsplit  9136  ssfzo12bi  9182  frecuzrdgfn  9356  ovshftex  9641
  Copyright terms: Public domain W3C validator