Theorem ssrdv 3244

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 3226	. 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 2203   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  eqelssd  3257  sscon  3353  ssdif  3354  unss1  3388  ssrin  3446  eq0rdv  3553  sspw  3682  uniss  3935  intss1  3964  intmin  3969  intssunim  3971  iunss1  4002  iinss1  4003  ss2iun  4006  ssiun  4033  ssiun2  4034  iinss  4043  iinss2  4044  exmidundif  4319  exmidundifim  4320  sspwb  4332  tron  4503  ssorduni  4609  ordsson  4614  ordpwsucss  4689  xpsspw  4862  relop  4905  dmss  4955  dmcosseq  5029  ssrnres  5205  chfnrn  5789  ffnfv  5835  f1imass  5947  fo1stresm  6355  fo2ndresm  6356  oprssdmm  6365  fo2ndf  6423  funsssuppss  6458  suppssdc  6460  suppssfvg  6463  reldmtpos  6484  smoiun  6532  tfrlemi14d  6564  tfr1onlemres  6580  tfri1dALT  6582  tfrcllemres  6593  dcdifsnid  6737  qsss  6828  pmss12g  6909  mapss  6926  ixpssmap2g  6962  ixpssmapg  6963  en2eqpr  7167  exmidpw  7168  exmidpweq  7169  onunsnss  7177  undifdcss  7183  ssfii  7261  fiss  7264  difinfsn  7391  addnqprlemrl  7872  addnqprlemru  7873  addnqprlemfl  7874  addnqprlemfu  7875  mulnqprlemrl  7888  mulnqprlemru  7889  mulnqprlemfl  7890  mulnqprlemfu  7891  distrlem1prl  7897  distrlem1pru  7898  distrlem5prl  7901  distrlem5pru  7902  ltprordil  7904  ltexprlemfl  7924  ltexprlemrl  7925  ltexprlemfu  7926  ltexprlemru  7927  addcanprleml  7929  addcanprlemu  7930  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  aptiprleml  7954  aptiprlemu  7955  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  cauappcvgprlemladdru  7971  cauappcvgprlemladdrl  7972  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  suplocexprlemss  8030  suplocexprlemex  8037  peano5uzti  9686  uzss  9875  ixxdisj  10236  ixxss1  10237  ixxss2  10238  ixxss12  10239  iocssre  10286  icossre  10287  iccssre  10288  icodisj  10325  fzss1  10397  fzss2  10398  fzoss1  10507  fzosplit  10513  fzouzsplit  10515  ssfzo12bi  10570  frecuzrdgtcl  10774  frecuzrdgdomlem  10779  sswrd  11233  ovshftex  11504  summodclem2a  12067  fsum3cvg3  12082  fsum2dlemstep  12120  prodmodclem2a  12262  fprod2dlemstep  12308  bitsfzo  12641  phimullem  12922  1arith  13065  ennnfonelemdm  13171  trivsubgsnd  13918  ssnmz  13928  trivnsgd  13934  kerf1ghm  13991  conjnmz  13996  unitssd  14254  subrguss  14381  unitrrg  14413  lsssssubg  14526  lssintclm  14532  zsssubrg  14733  mulgrhm2  14758  znrrg  14808  psrbaglesuppg  14821  bastg  14926  tgss  14928  tgtop  14933  tgidm  14939  neisspw  15013  topssnei  15027  tgrest  15034  ssrest  15047  cnss1  15091  cnss2  15092  cnsscnp  15094  cnrest2r  15102  txdis  15142  xblss2ps  15269  xblss2  15270  xmettxlem  15374  xmettx  15375  cncfss  15448  cnopnap  15476  dvfgg  15553  dvcj  15574  usgruspgrben  16181  uhgrissubgr  16256  uhgrspansubgrlem  16271