Theorem ssrdv 3199

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 1897	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3181	. 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 1371   e. wcel 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqelssd  3212  sscon  3307  ssdif  3308  unss1  3342  ssrin  3398  eq0rdv  3505  uniss  3871  intss1  3900  intmin  3905  intssunim  3907  iunss1  3938  iinss1  3939  ss2iun  3942  ssiun  3969  ssiun2  3970  iinss  3979  iinss2  3980  exmidundif  4251  exmidundifim  4252  sspwb  4261  tron  4430  ssorduni  4536  ordsson  4541  ordpwsucss  4616  xpsspw  4788  relop  4829  dmss  4878  dmcosseq  4951  ssrnres  5126  chfnrn  5693  ffnfv  5740  f1imass  5845  fo1stresm  6249  fo2ndresm  6250  oprssdmm  6259  fo2ndf  6315  reldmtpos  6341  smoiun  6389  tfrlemi14d  6421  tfr1onlemres  6437  tfri1dALT  6439  tfrcllemres  6450  dcdifsnid  6592  qsss  6683  pmss12g  6764  mapss  6780  ixpssmap2g  6816  ixpssmapg  6817  en2eqpr  7006  exmidpw  7007  exmidpweq  7008  onunsnss  7016  undifdcss  7022  ssfii  7078  fiss  7081  difinfsn  7204  addnqprlemrl  7672  addnqprlemru  7673  addnqprlemfl  7674  addnqprlemfu  7675  mulnqprlemrl  7688  mulnqprlemru  7689  mulnqprlemfl  7690  mulnqprlemfu  7691  distrlem1prl  7697  distrlem1pru  7698  distrlem5prl  7701  distrlem5pru  7702  ltprordil  7704  ltexprlemfl  7724  ltexprlemrl  7725  ltexprlemfu  7726  ltexprlemru  7727  addcanprleml  7729  addcanprlemu  7730  recexprlem1ssl  7748  recexprlem1ssu  7749  recexprlemss1l  7750  recexprlemss1u  7751  aptiprleml  7754  aptiprlemu  7755  cauappcvgprlemladdfu  7769  cauappcvgprlemladdfl  7770  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  suplocexprlemss  7830  suplocexprlemex  7837  peano5uzti  9483  uzss  9671  ixxdisj  10027  ixxss1  10028  ixxss2  10029  ixxss12  10030  iocssre  10077  icossre  10078  iccssre  10079  icodisj  10116  fzss1  10187  fzss2  10188  fzoss1  10297  fzosplit  10303  fzouzsplit  10305  ssfzo12bi  10356  frecuzrdgtcl  10559  frecuzrdgdomlem  10564  sswrd  11005  ovshftex  11163  summodclem2a  11725  fsum3cvg3  11740  fsum2dlemstep  11778  prodmodclem2a  11920  fprod2dlemstep  11966  bitsfzo  12299  phimullem  12580  1arith  12723  ennnfonelemdm  12824  trivsubgsnd  13570  ssnmz  13580  trivnsgd  13586  kerf1ghm  13643  conjnmz  13648  unitssd  13904  subrguss  14031  unitrrg  14062  lsssssubg  14173  lssintclm  14179  zsssubrg  14380  mulgrhm2  14405  znrrg  14455  psrbaglesuppg  14467  bastg  14566  tgss  14568  tgtop  14573  tgidm  14579  neisspw  14653  topssnei  14667  tgrest  14674  ssrest  14687  cnss1  14731  cnss2  14732  cnsscnp  14734  cnrest2r  14742  txdis  14782  xblss2ps  14909  xblss2  14910  xmettxlem  15014  xmettx  15015  cncfss  15088  cnopnap  15116  dvfgg  15193  dvcj  15214