Theorem ssrdv 3161

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 1874	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3144	. 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 1351   e. wcel 2148   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  eqelssd  3174  sscon  3269  ssdif  3270  unss1  3304  ssrin  3360  eq0rdv  3467  uniss  3830  intss1  3859  intmin  3864  intssunim  3866  iunss1  3897  iinss1  3898  ss2iun  3901  ssiun  3928  ssiun2  3929  iinss  3938  iinss2  3939  exmidundif  4206  exmidundifim  4207  sspwb  4216  tron  4382  ssorduni  4486  ordsson  4491  ordpwsucss  4566  xpsspw  4738  relop  4777  dmss  4826  dmcosseq  4898  ssrnres  5071  chfnrn  5627  ffnfv  5674  f1imass  5774  fo1stresm  6161  fo2ndresm  6162  oprssdmm  6171  fo2ndf  6227  reldmtpos  6253  smoiun  6301  tfrlemi14d  6333  tfr1onlemres  6349  tfri1dALT  6351  tfrcllemres  6362  dcdifsnid  6504  qsss  6593  pmss12g  6674  mapss  6690  ixpssmap2g  6726  ixpssmapg  6727  en2eqpr  6906  exmidpw  6907  exmidpweq  6908  onunsnss  6915  undifdcss  6921  ssfii  6972  fiss  6975  difinfsn  7098  addnqprlemrl  7555  addnqprlemru  7556  addnqprlemfl  7557  addnqprlemfu  7558  mulnqprlemrl  7571  mulnqprlemru  7572  mulnqprlemfl  7573  mulnqprlemfu  7574  distrlem1prl  7580  distrlem1pru  7581  distrlem5prl  7584  distrlem5pru  7585  ltprordil  7587  ltexprlemfl  7607  ltexprlemrl  7608  ltexprlemfu  7609  ltexprlemru  7610  addcanprleml  7612  addcanprlemu  7613  recexprlem1ssl  7631  recexprlem1ssu  7632  recexprlemss1l  7633  recexprlemss1u  7634  aptiprleml  7637  aptiprlemu  7638  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  suplocexprlemss  7713  suplocexprlemex  7720  peano5uzti  9360  uzss  9547  ixxdisj  9902  ixxss1  9903  ixxss2  9904  ixxss12  9905  iocssre  9952  icossre  9953  iccssre  9954  icodisj  9991  fzss1  10062  fzss2  10063  fzoss1  10170  fzosplit  10176  fzouzsplit  10178  ssfzo12bi  10224  frecuzrdgtcl  10411  frecuzrdgdomlem  10416  ovshftex  10827  summodclem2a  11388  fsum3cvg3  11403  fsum2dlemstep  11441  prodmodclem2a  11583  fprod2dlemstep  11629  phimullem  12224  1arith  12364  ennnfonelemdm  12420  trivsubgsnd  13059  ssnmz  13069  trivnsgd  13075  unitssd  13276  subrguss  13355  zsssubrg  13449  bastg  13531  tgss  13533  tgtop  13538  tgidm  13544  neisspw  13618  topssnei  13632  tgrest  13639  ssrest  13652  cnss1  13696  cnss2  13697  cnsscnp  13699  cnrest2r  13707  txdis  13747  xblss2ps  13874  xblss2  13875  xmettxlem  13979  xmettx  13980  cncfss  14040  cnopnap  14064  dvfgg  14127  dvcj  14143