Theorem ssrdv 3154

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 1868	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3137	. 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 1347   e. wcel 2142   C_ wss 3122

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 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-11 1500  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-ext 2153

This theorem depends on definitions:  df-bi 116  df-nf 1455  df-sb 1757  df-clab 2158  df-cleq 2164  df-clel 2167  df-in 3128  df-ss 3135

This theorem is referenced by:  eqelssd  3167  sscon  3262  ssdif  3263  unss1  3297  ssrin  3353  eq0rdv  3460  uniss  3818  intss1  3847  intmin  3852  intssunim  3854  iunss1  3885  iinss1  3886  ss2iun  3889  ssiun  3916  ssiun2  3917  iinss  3925  iinss2  3926  exmidundif  4193  exmidundifim  4194  sspwb  4202  tron  4368  ssorduni  4472  ordsson  4477  ordpwsucss  4552  xpsspw  4724  relop  4762  dmss  4811  dmcosseq  4883  ssrnres  5055  chfnrn  5611  ffnfv  5658  f1imass  5757  fo1stresm  6144  fo2ndresm  6145  oprssdmm  6154  fo2ndf  6210  reldmtpos  6236  smoiun  6284  tfrlemi14d  6316  tfr1onlemres  6332  tfri1dALT  6334  tfrcllemres  6345  dcdifsnid  6487  qsss  6576  pmss12g  6657  mapss  6673  ixpssmap2g  6709  ixpssmapg  6710  en2eqpr  6889  exmidpw  6890  exmidpweq  6891  onunsnss  6898  undifdcss  6904  ssfii  6955  fiss  6958  difinfsn  7081  addnqprlemrl  7523  addnqprlemru  7524  addnqprlemfl  7525  addnqprlemfu  7526  mulnqprlemrl  7539  mulnqprlemru  7540  mulnqprlemfl  7541  mulnqprlemfu  7542  distrlem1prl  7548  distrlem1pru  7549  distrlem5prl  7552  distrlem5pru  7553  ltprordil  7555  ltexprlemfl  7575  ltexprlemrl  7576  ltexprlemfu  7577  ltexprlemru  7578  addcanprleml  7580  addcanprlemu  7581  recexprlem1ssl  7599  recexprlem1ssu  7600  recexprlemss1l  7601  recexprlemss1u  7602  aptiprleml  7605  aptiprlemu  7606  cauappcvgprlemladdfu  7620  cauappcvgprlemladdfl  7621  cauappcvgprlemladdru  7622  cauappcvgprlemladdrl  7623  caucvgprlemladdfu  7643  caucvgprlemladdrl  7644  suplocexprlemss  7681  suplocexprlemex  7688  peano5uzti  9324  uzss  9511  ixxdisj  9864  ixxss1  9865  ixxss2  9866  ixxss12  9867  iocssre  9914  icossre  9915  iccssre  9916  icodisj  9953  fzss1  10023  fzss2  10024  fzoss1  10131  fzosplit  10137  fzouzsplit  10139  ssfzo12bi  10185  frecuzrdgtcl  10372  frecuzrdgdomlem  10377  ovshftex  10787  summodclem2a  11348  fsum3cvg3  11363  fsum2dlemstep  11401  prodmodclem2a  11543  fprod2dlemstep  11589  phimullem  12183  1arith  12323  ennnfonelemdm  12379  bastg  12940  tgss  12942  tgtop  12947  tgidm  12953  neisspw  13027  topssnei  13041  tgrest  13048  ssrest  13061  cnss1  13105  cnss2  13106  cnsscnp  13108  cnrest2r  13116  txdis  13156  xblss2ps  13283  xblss2  13284  xmettxlem  13388  xmettx  13389  cncfss  13449  cnopnap  13473  dvfgg  13536  dvcj  13552