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

Theorem ssrdv 3020
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 1799 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3003 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 132 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285    e. wcel 1436    C_ wss 2988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2994  df-ss 3001
This theorem is referenced by:  sscon  3123  ssdif  3124  unss1  3158  ssrin  3214  eq0rdv  3315  uniss  3657  intss1  3686  intmin  3691  intssunim  3693  iunss1  3724  iinss1  3725  ss2iun  3728  ssiun  3755  ssiun2  3756  iinss  3764  iinss2  3765  trintssmOLD  3928  exmidundif  4009  sspwb  4017  tron  4183  ssorduni  4277  ordsson  4282  ordpwsucss  4356  xpsspw  4518  relop  4554  dmss  4603  dmcosseq  4672  ssrnres  4839  chfnrn  5373  ffnfv  5419  f1imass  5514  fo1stresm  5889  fo2ndresm  5890  fo2ndf  5949  reldmtpos  5972  smoiun  6020  tfrlemi14d  6052  tfr1onlemres  6068  tfri1dALT  6070  tfrcllemres  6081  dcdifsnid  6217  qsss  6303  pmss12g  6384  mapss  6400  en2eqpr  6575  exmidpw  6576  onunsnss  6579  undifdcss  6585  addnqprlemrl  7060  addnqprlemru  7061  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemrl  7076  mulnqprlemru  7077  mulnqprlemfl  7078  mulnqprlemfu  7079  distrlem1prl  7085  distrlem1pru  7086  distrlem5prl  7089  distrlem5pru  7090  ltprordil  7092  ltexprlemfl  7112  ltexprlemrl  7113  ltexprlemfu  7114  ltexprlemru  7115  addcanprleml  7117  addcanprlemu  7118  recexprlem1ssl  7136  recexprlem1ssu  7137  recexprlemss1l  7138  recexprlemss1u  7139  aptiprleml  7142  aptiprlemu  7143  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  caucvgprlemladdfu  7180  caucvgprlemladdrl  7181  peano5uzti  8787  uzss  8971  ixxdisj  9253  ixxss1  9254  ixxss2  9255  ixxss12  9256  iocssre  9303  icossre  9304  iccssre  9305  icodisj  9341  fzss1  9408  fzss2  9409  fzoss1  9510  fzosplit  9516  fzouzsplit  9518  ssfzo12bi  9564  frecuzrdgtcl  9747  frecuzrdgdomlem  9752  ovshftex  10149  isummolem2a  10660  phimullem  11076
  Copyright terms: Public domain W3C validator