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

Theorem ssrdv 3014
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 1797 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 2997 . 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 1283    e. wcel 1434    C_ wss 2982
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 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2988  df-ss 2995
This theorem is referenced by:  sscon  3116  ssdif  3117  unss1  3151  ssrin  3207  eq0rdv  3304  uniss  3642  intss1  3671  intmin  3676  intssunim  3678  iunss1  3709  iinss1  3710  ss2iun  3713  ssiun  3740  ssiun2  3741  iinss  3749  iinss2  3750  trintssmOLD  3912  exmidundif  3991  sspwb  3999  tron  4165  ssorduni  4259  ordsson  4264  ordpwsucss  4338  xpsspw  4498  relop  4534  dmss  4582  dmcosseq  4651  ssrnres  4813  chfnrn  5330  ffnfv  5375  f1imass  5465  fo1stresm  5839  fo2ndresm  5840  fo2ndf  5899  reldmtpos  5922  smoiun  5970  tfrlemi14d  6002  tfr1onlemres  6018  tfri1dALT  6020  tfrcllemres  6031  dcdifsnid  6166  qsss  6252  en2eqpr  6458  onunsnss  6461  undifdcss  6467  addnqprlemrl  6861  addnqprlemru  6862  addnqprlemfl  6863  addnqprlemfu  6864  mulnqprlemrl  6877  mulnqprlemru  6878  mulnqprlemfl  6879  mulnqprlemfu  6880  distrlem1prl  6886  distrlem1pru  6887  distrlem5prl  6890  distrlem5pru  6891  ltprordil  6893  ltexprlemfl  6913  ltexprlemrl  6914  ltexprlemfu  6915  ltexprlemru  6916  addcanprleml  6918  addcanprlemu  6919  recexprlem1ssl  6937  recexprlem1ssu  6938  recexprlemss1l  6939  recexprlemss1u  6940  aptiprleml  6943  aptiprlemu  6944  cauappcvgprlemladdfu  6958  cauappcvgprlemladdfl  6959  cauappcvgprlemladdru  6960  cauappcvgprlemladdrl  6961  caucvgprlemladdfu  6981  caucvgprlemladdrl  6982  peano5uzti  8588  uzss  8772  ixxdisj  9054  ixxss1  9055  ixxss2  9056  ixxss12  9057  iocssre  9104  icossre  9105  iccssre  9106  icodisj  9142  fzss1  9209  fzss2  9210  fzoss1  9309  fzosplit  9315  fzouzsplit  9317  ssfzo12bi  9363  frecuzrdgtcl  9546  frecuzrdgdomlem  9551  ovshftex  9908  phimullem  10808
  Copyright terms: Public domain W3C validator