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

Theorem ssrdv 3103
Description: Deduction 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 1846 . 2  |-  ( ph  ->  A. x ( x  e.  A  ->  x  e.  B ) )
3 dfss2 3086 . 2  |-  ( A 
C_  B  <->  A. x
( x  e.  A  ->  x  e.  B ) )
42, 3sylibr 133 1  |-  ( ph  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1329    e. wcel 1480    C_ wss 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  eqelssd  3116  sscon  3210  ssdif  3211  unss1  3245  ssrin  3301  eq0rdv  3407  uniss  3757  intss1  3786  intmin  3791  intssunim  3793  iunss1  3824  iinss1  3825  ss2iun  3828  ssiun  3855  ssiun2  3856  iinss  3864  iinss2  3865  exmidundif  4129  exmidundifim  4130  sspwb  4138  tron  4304  ssorduni  4403  ordsson  4408  ordpwsucss  4482  xpsspw  4651  relop  4689  dmss  4738  dmcosseq  4810  ssrnres  4981  chfnrn  5531  ffnfv  5578  f1imass  5675  fo1stresm  6059  fo2ndresm  6060  oprssdmm  6069  fo2ndf  6124  reldmtpos  6150  smoiun  6198  tfrlemi14d  6230  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemres  6259  dcdifsnid  6400  qsss  6488  pmss12g  6569  mapss  6585  ixpssmap2g  6621  ixpssmapg  6622  en2eqpr  6801  exmidpw  6802  onunsnss  6805  undifdcss  6811  ssfii  6862  fiss  6865  difinfsn  6985  addnqprlemrl  7377  addnqprlemru  7378  addnqprlemfl  7379  addnqprlemfu  7380  mulnqprlemrl  7393  mulnqprlemru  7394  mulnqprlemfl  7395  mulnqprlemfu  7396  distrlem1prl  7402  distrlem1pru  7403  distrlem5prl  7406  distrlem5pru  7407  ltprordil  7409  ltexprlemfl  7429  ltexprlemrl  7430  ltexprlemfu  7431  ltexprlemru  7432  addcanprleml  7434  addcanprlemu  7435  recexprlem1ssl  7453  recexprlem1ssu  7454  recexprlemss1l  7455  recexprlemss1u  7456  aptiprleml  7459  aptiprlemu  7460  cauappcvgprlemladdfu  7474  cauappcvgprlemladdfl  7475  cauappcvgprlemladdru  7476  cauappcvgprlemladdrl  7477  caucvgprlemladdfu  7497  caucvgprlemladdrl  7498  suplocexprlemss  7535  suplocexprlemex  7542  peano5uzti  9171  uzss  9358  ixxdisj  9698  ixxss1  9699  ixxss2  9700  ixxss12  9701  iocssre  9748  icossre  9749  iccssre  9750  icodisj  9787  fzss1  9855  fzss2  9856  fzoss1  9960  fzosplit  9966  fzouzsplit  9968  ssfzo12bi  10014  frecuzrdgtcl  10197  frecuzrdgdomlem  10202  ovshftex  10603  summodclem2a  11162  fsum3cvg3  11177  fsum2dlemstep  11215  prodmodclem2a  11357  phimullem  11912  ennnfonelemdm  11944  bastg  12244  tgss  12246  tgtop  12251  tgidm  12257  neisspw  12331  topssnei  12345  tgrest  12352  ssrest  12365  cnss1  12409  cnss2  12410  cnsscnp  12412  cnrest2r  12420  txdis  12460  xblss2ps  12587  xblss2  12588  xmettxlem  12692  xmettx  12693  cncfss  12753  cnopnap  12777  dvfgg  12840  dvcj  12856
  Copyright terms: Public domain W3C validator