Theorem ssrdv 3248

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 1923	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3229	. 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 1396   e. wcel 2205   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  eqelssd  3261  sscon  3357  ssdif  3358  unss1  3392  ssrin  3450  eq0rdv  3557  sspw  3687  uniss  3940  intss1  3969  intmin  3974  intssunim  3976  iunss1  4007  iinss1  4008  ss2iun  4011  ssiun  4038  ssiun2  4039  iinss  4048  iinss2  4049  exmidundif  4324  exmidundifim  4325  sspwb  4337  tron  4508  ssorduni  4614  ordsson  4619  ordpwsucss  4694  xpsspw  4867  relop  4910  dmss  4960  dmcosseq  5034  ssrnres  5210  chfnrn  5794  ffnfv  5840  f1imass  5953  abrexss  6331  fo1stresm  6368  fo2ndresm  6369  oprssdmm  6378  fo2ndf  6436  funsssuppss  6471  suppssdc  6473  suppssfvg  6476  reldmtpos  6497  smoiun  6545  tfrlemi14d  6577  tfr1onlemres  6593  tfri1dALT  6595  tfrcllemres  6606  dcdifsnid  6750  qsss  6841  pmss12g  6922  mapss  6939  ixpssmap2g  6975  ixpssmapg  6976  en2eqpr  7180  exmidpw  7181  exmidpweq  7182  onunsnss  7190  undifdcss  7196  ssfii  7274  fiss  7277  difinfsn  7404  addnqprlemrl  7888  addnqprlemru  7889  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemrl  7904  mulnqprlemru  7905  mulnqprlemfl  7906  mulnqprlemfu  7907  distrlem1prl  7913  distrlem1pru  7914  distrlem5prl  7917  distrlem5pru  7918  ltprordil  7920  ltexprlemfl  7940  ltexprlemrl  7941  ltexprlemfu  7942  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  recexprlem1ssl  7964  recexprlem1ssu  7965  recexprlemss1l  7966  recexprlemss1u  7967  aptiprleml  7970  aptiprlemu  7971  cauappcvgprlemladdfu  7985  cauappcvgprlemladdfl  7986  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  suplocexprlemss  8046  suplocexprlemex  8053  peano5uzti  9704  uzss  9893  ixxdisj  10255  ixxss1  10256  ixxss2  10257  ixxss12  10258  iocssre  10305  icossre  10306  iccssre  10307  icodisj  10344  fzss1  10418  fzss2  10419  fzoss1  10529  fzosplit  10535  fzouzsplit  10537  ssfzo12bi  10592  frecuzrdgtcl  10798  frecuzrdgdomlem  10803  sswrd  11258  ovshftex  11529  summodclem2a  12092  fsum3cvg3  12107  fsum2dlemstep  12145  prodmodclem2a  12287  fprod2dlemstep  12333  bitsfzo  12666  phimullem  12947  1arith  13090  ennnfonelemdm  13255  trivsubgsnd  13954  ssnmz  13964  trivnsgd  13970  kerf1ghm  14027  conjnmz  14032  unitssd  14354  subrguss  14482  unitrrg  14514  lsssssubg  14652  lssintclm  14658  zsssubrg  14859  mulgrhm2  14884  znrrg  14934  psrbaglesuppg  14947  bastg  15052  tgss  15054  tgtop  15059  tgidm  15065  neisspw  15139  topssnei  15153  tgrest  15160  ssrest  15173  cnss1  15217  cnss2  15218  cnsscnp  15220  cnrest2r  15228  txdis  15268  xblss2ps  15395  xblss2  15396  xmettxlem  15500  xmettx  15501  cncfss  15574  cnopnap  15602  dvfgg  15679  dvcj  15700  usgruspgrben  16307  uhgrissubgr  16382  uhgrspansubgrlem  16397