Theorem ssrdv 3234

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 1922	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3216	. 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 2202   C_ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqelssd  3247  sscon  3343  ssdif  3344  unss1  3378  ssrin  3434  eq0rdv  3541  uniss  3919  intss1  3948  intmin  3953  intssunim  3955  iunss1  3986  iinss1  3987  ss2iun  3990  ssiun  4017  ssiun2  4018  iinss  4027  iinss2  4028  exmidundif  4302  exmidundifim  4303  sspwb  4314  tron  4485  ssorduni  4591  ordsson  4596  ordpwsucss  4671  xpsspw  4844  relop  4886  dmss  4936  dmcosseq  5010  ssrnres  5186  chfnrn  5767  ffnfv  5813  f1imass  5925  fo1stresm  6333  fo2ndresm  6334  oprssdmm  6343  fo2ndf  6401  funsssuppss  6436  suppssdc  6438  suppssfvg  6441  reldmtpos  6462  smoiun  6510  tfrlemi14d  6542  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemres  6571  dcdifsnid  6715  qsss  6806  pmss12g  6887  mapss  6903  ixpssmap2g  6939  ixpssmapg  6940  en2eqpr  7142  exmidpw  7143  exmidpweq  7144  onunsnss  7152  undifdcss  7158  ssfii  7233  fiss  7236  difinfsn  7359  addnqprlemrl  7837  addnqprlemru  7838  addnqprlemfl  7839  addnqprlemfu  7840  mulnqprlemrl  7853  mulnqprlemru  7854  mulnqprlemfl  7855  mulnqprlemfu  7856  distrlem1prl  7862  distrlem1pru  7863  distrlem5prl  7866  distrlem5pru  7867  ltprordil  7869  ltexprlemfl  7889  ltexprlemrl  7890  ltexprlemfu  7891  ltexprlemru  7892  addcanprleml  7894  addcanprlemu  7895  recexprlem1ssl  7913  recexprlem1ssu  7914  recexprlemss1l  7915  recexprlemss1u  7916  aptiprleml  7919  aptiprlemu  7920  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprlemladdfu  7957  caucvgprlemladdrl  7958  suplocexprlemss  7995  suplocexprlemex  8002  peano5uzti  9649  uzss  9838  ixxdisj  10199  ixxss1  10200  ixxss2  10201  ixxss12  10202  iocssre  10249  icossre  10250  iccssre  10251  icodisj  10288  fzss1  10360  fzss2  10361  fzoss1  10470  fzosplit  10476  fzouzsplit  10478  ssfzo12bi  10533  frecuzrdgtcl  10737  frecuzrdgdomlem  10742  sswrd  11188  ovshftex  11459  summodclem2a  12022  fsum3cvg3  12037  fsum2dlemstep  12075  prodmodclem2a  12217  fprod2dlemstep  12263  bitsfzo  12596  phimullem  12877  1arith  13020  ennnfonelemdm  13121  trivsubgsnd  13868  ssnmz  13878  trivnsgd  13884  kerf1ghm  13941  conjnmz  13946  unitssd  14204  subrguss  14331  unitrrg  14363  lsssssubg  14474  lssintclm  14480  zsssubrg  14681  mulgrhm2  14706  znrrg  14756  psrbaglesuppg  14768  bastg  14872  tgss  14874  tgtop  14879  tgidm  14885  neisspw  14959  topssnei  14973  tgrest  14980  ssrest  14993  cnss1  15037  cnss2  15038  cnsscnp  15040  cnrest2r  15048  txdis  15088  xblss2ps  15215  xblss2  15216  xmettxlem  15320  xmettx  15321  cncfss  15394  cnopnap  15422  dvfgg  15499  dvcj  15520  usgruspgrben  16127  uhgrissubgr  16202  uhgrspansubgrlem  16217