Theorem ssrdv 3153

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

Syntax hints:   -> wi 4   A.wal 1346   e. wcel 2141   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  eqelssd  3166  sscon  3261  ssdif  3262  unss1  3296  ssrin  3352  eq0rdv  3458  uniss  3815  intss1  3844  intmin  3849  intssunim  3851  iunss1  3882  iinss1  3883  ss2iun  3886  ssiun  3913  ssiun2  3914  iinss  3922  iinss2  3923  exmidundif  4190  exmidundifim  4191  sspwb  4199  tron  4365  ssorduni  4469  ordsson  4474  ordpwsucss  4549  xpsspw  4721  relop  4759  dmss  4808  dmcosseq  4880  ssrnres  5051  chfnrn  5604  ffnfv  5651  f1imass  5750  fo1stresm  6137  fo2ndresm  6138  oprssdmm  6147  fo2ndf  6203  reldmtpos  6229  smoiun  6277  tfrlemi14d  6309  tfr1onlemres  6325  tfri1dALT  6327  tfrcllemres  6338  dcdifsnid  6480  qsss  6568  pmss12g  6649  mapss  6665  ixpssmap2g  6701  ixpssmapg  6702  en2eqpr  6881  exmidpw  6882  exmidpweq  6883  onunsnss  6890  undifdcss  6896  ssfii  6947  fiss  6950  difinfsn  7073  addnqprlemrl  7506  addnqprlemru  7507  addnqprlemfl  7508  addnqprlemfu  7509  mulnqprlemrl  7522  mulnqprlemru  7523  mulnqprlemfl  7524  mulnqprlemfu  7525  distrlem1prl  7531  distrlem1pru  7532  distrlem5prl  7535  distrlem5pru  7536  ltprordil  7538  ltexprlemfl  7558  ltexprlemrl  7559  ltexprlemfu  7560  ltexprlemru  7561  addcanprleml  7563  addcanprlemu  7564  recexprlem1ssl  7582  recexprlem1ssu  7583  recexprlemss1l  7584  recexprlemss1u  7585  aptiprleml  7588  aptiprlemu  7589  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  cauappcvgprlemladdru  7605  cauappcvgprlemladdrl  7606  caucvgprlemladdfu  7626  caucvgprlemladdrl  7627  suplocexprlemss  7664  suplocexprlemex  7671  peano5uzti  9307  uzss  9494  ixxdisj  9847  ixxss1  9848  ixxss2  9849  ixxss12  9850  iocssre  9897  icossre  9898  iccssre  9899  icodisj  9936  fzss1  10006  fzss2  10007  fzoss1  10114  fzosplit  10120  fzouzsplit  10122  ssfzo12bi  10168  frecuzrdgtcl  10355  frecuzrdgdomlem  10360  ovshftex  10770  summodclem2a  11331  fsum3cvg3  11346  fsum2dlemstep  11384  prodmodclem2a  11526  fprod2dlemstep  11572  phimullem  12166  1arith  12306  ennnfonelemdm  12362  bastg  12776  tgss  12778  tgtop  12783  tgidm  12789  neisspw  12863  topssnei  12877  tgrest  12884  ssrest  12897  cnss1  12941  cnss2  12942  cnsscnp  12944  cnrest2r  12952  txdis  12992  xblss2ps  13119  xblss2  13120  xmettxlem  13224  xmettx  13225  cncfss  13285  cnopnap  13309  dvfgg  13372  dvcj  13388