Theorem ssrdv 3176

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 1885	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3159	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4	2, 3	sylibr 134	1 |- ( ph -> A C_ B )

Syntax hints:   -> wi 4   A.wal 1362   e. wcel 2160   C_ wss 3144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  eqelssd  3189  sscon  3284  ssdif  3285  unss1  3319  ssrin  3375  eq0rdv  3482  uniss  3845  intss1  3874  intmin  3879  intssunim  3881  iunss1  3912  iinss1  3913  ss2iun  3916  ssiun  3943  ssiun2  3944  iinss  3953  iinss2  3954  exmidundif  4221  exmidundifim  4222  sspwb  4231  tron  4397  ssorduni  4501  ordsson  4506  ordpwsucss  4581  xpsspw  4753  relop  4792  dmss  4841  dmcosseq  4913  ssrnres  5086  chfnrn  5643  ffnfv  5690  f1imass  5791  fo1stresm  6180  fo2ndresm  6181  oprssdmm  6190  fo2ndf  6246  reldmtpos  6272  smoiun  6320  tfrlemi14d  6352  tfr1onlemres  6368  tfri1dALT  6370  tfrcllemres  6381  dcdifsnid  6523  qsss  6612  pmss12g  6693  mapss  6709  ixpssmap2g  6745  ixpssmapg  6746  en2eqpr  6925  exmidpw  6926  exmidpweq  6927  onunsnss  6934  undifdcss  6940  ssfii  6991  fiss  6994  difinfsn  7117  addnqprlemrl  7574  addnqprlemru  7575  addnqprlemfl  7576  addnqprlemfu  7577  mulnqprlemrl  7590  mulnqprlemru  7591  mulnqprlemfl  7592  mulnqprlemfu  7593  distrlem1prl  7599  distrlem1pru  7600  distrlem5prl  7603  distrlem5pru  7604  ltprordil  7606  ltexprlemfl  7626  ltexprlemrl  7627  ltexprlemfu  7628  ltexprlemru  7629  addcanprleml  7631  addcanprlemu  7632  recexprlem1ssl  7650  recexprlem1ssu  7651  recexprlemss1l  7652  recexprlemss1u  7653  aptiprleml  7656  aptiprlemu  7657  cauappcvgprlemladdfu  7671  cauappcvgprlemladdfl  7672  cauappcvgprlemladdru  7673  cauappcvgprlemladdrl  7674  caucvgprlemladdfu  7694  caucvgprlemladdrl  7695  suplocexprlemss  7732  suplocexprlemex  7739  peano5uzti  9379  uzss  9566  ixxdisj  9921  ixxss1  9922  ixxss2  9923  ixxss12  9924  iocssre  9971  icossre  9972  iccssre  9973  icodisj  10010  fzss1  10081  fzss2  10082  fzoss1  10189  fzosplit  10195  fzouzsplit  10197  ssfzo12bi  10243  frecuzrdgtcl  10430  frecuzrdgdomlem  10435  ovshftex  10846  summodclem2a  11407  fsum3cvg3  11422  fsum2dlemstep  11460  prodmodclem2a  11602  fprod2dlemstep  11648  phimullem  12243  1arith  12383  ennnfonelemdm  12439  trivsubgsnd  13106  ssnmz  13116  trivnsgd  13122  kerf1ghm  13174  conjnmz  13179  unitssd  13420  subrguss  13544  lsssssubg  13655  lssintclm  13661  zsssubrg  13849  mulgrhm2  13869  bastg  13958  tgss  13960  tgtop  13965  tgidm  13971  neisspw  14045  topssnei  14059  tgrest  14066  ssrest  14079  cnss1  14123  cnss2  14124  cnsscnp  14126  cnrest2r  14134  txdis  14174  xblss2ps  14301  xblss2  14302  xmettxlem  14406  xmettx  14407  cncfss  14467  cnopnap  14491  dvfgg  14554  dvcj  14570