Theorem ssrdv 3148

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

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 |- ( ph -> ( x e. A -> x e. B ) )
2	1	alrimiv 1862	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3131	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4	2, 3	sylibr 133	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   A.wal 1341   e. wcel 2136   C_ wss 3116

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  eqelssd  3161  sscon  3256  ssdif  3257  unss1  3291  ssrin  3347  eq0rdv  3453  uniss  3810  intss1  3839  intmin  3844  intssunim  3846  iunss1  3877  iinss1  3878  ss2iun  3881  ssiun  3908  ssiun2  3909  iinss  3917  iinss2  3918  exmidundif  4185  exmidundifim  4186  sspwb  4194  tron  4360  ssorduni  4464  ordsson  4469  ordpwsucss  4544  xpsspw  4716  relop  4754  dmss  4803  dmcosseq  4875  ssrnres  5046  chfnrn  5596  ffnfv  5643  f1imass  5742  fo1stresm  6129  fo2ndresm  6130  oprssdmm  6139  fo2ndf  6195  reldmtpos  6221  smoiun  6269  tfrlemi14d  6301  tfr1onlemres  6317  tfri1dALT  6319  tfrcllemres  6330  dcdifsnid  6472  qsss  6560  pmss12g  6641  mapss  6657  ixpssmap2g  6693  ixpssmapg  6694  en2eqpr  6873  exmidpw  6874  exmidpweq  6875  onunsnss  6882  undifdcss  6888  ssfii  6939  fiss  6942  difinfsn  7065  addnqprlemrl  7498  addnqprlemru  7499  addnqprlemfl  7500  addnqprlemfu  7501  mulnqprlemrl  7514  mulnqprlemru  7515  mulnqprlemfl  7516  mulnqprlemfu  7517  distrlem1prl  7523  distrlem1pru  7524  distrlem5prl  7527  distrlem5pru  7528  ltprordil  7530  ltexprlemfl  7550  ltexprlemrl  7551  ltexprlemfu  7552  ltexprlemru  7553  addcanprleml  7555  addcanprlemu  7556  recexprlem1ssl  7574  recexprlem1ssu  7575  recexprlemss1l  7576  recexprlemss1u  7577  aptiprleml  7580  aptiprlemu  7581  cauappcvgprlemladdfu  7595  cauappcvgprlemladdfl  7596  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  suplocexprlemss  7656  suplocexprlemex  7663  peano5uzti  9299  uzss  9486  ixxdisj  9839  ixxss1  9840  ixxss2  9841  ixxss12  9842  iocssre  9889  icossre  9890  iccssre  9891  icodisj  9928  fzss1  9998  fzss2  9999  fzoss1  10106  fzosplit  10112  fzouzsplit  10114  ssfzo12bi  10160  frecuzrdgtcl  10347  frecuzrdgdomlem  10352  ovshftex  10761  summodclem2a  11322  fsum3cvg3  11337  fsum2dlemstep  11375  prodmodclem2a  11517  fprod2dlemstep  11563  phimullem  12157  1arith  12297  ennnfonelemdm  12353  bastg  12701  tgss  12703  tgtop  12708  tgidm  12714  neisspw  12788  topssnei  12802  tgrest  12809  ssrest  12822  cnss1  12866  cnss2  12867  cnsscnp  12869  cnrest2r  12877  txdis  12917  xblss2ps  13044  xblss2  13045  xmettxlem  13149  xmettx  13150  cncfss  13210  cnopnap  13234  dvfgg  13297  dvcj  13313