Theorem ssrdv 3053

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 1813	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3036	. 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 1297   e. wcel 1448   C_ wss 3021

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034

This theorem is referenced by:  eqelssd  3066  sscon  3157  ssdif  3158  unss1  3192  ssrin  3248  eq0rdv  3354  uniss  3704  intss1  3733  intmin  3738  intssunim  3740  iunss1  3771  iinss1  3772  ss2iun  3775  ssiun  3802  ssiun2  3803  iinss  3811  iinss2  3812  exmidundif  4067  exmidundifim  4068  sspwb  4076  tron  4242  ssorduni  4341  ordsson  4346  ordpwsucss  4420  xpsspw  4589  relop  4627  dmss  4676  dmcosseq  4746  ssrnres  4917  chfnrn  5463  ffnfv  5510  f1imass  5607  fo1stresm  5990  fo2ndresm  5991  fo2ndf  6054  reldmtpos  6080  smoiun  6128  tfrlemi14d  6160  tfr1onlemres  6176  tfri1dALT  6178  tfrcllemres  6189  dcdifsnid  6330  qsss  6418  pmss12g  6499  mapss  6515  ixpssmap2g  6551  ixpssmapg  6552  en2eqpr  6730  exmidpw  6731  onunsnss  6734  undifdcss  6740  difinfsn  6900  addnqprlemrl  7266  addnqprlemru  7267  addnqprlemfl  7268  addnqprlemfu  7269  mulnqprlemrl  7282  mulnqprlemru  7283  mulnqprlemfl  7284  mulnqprlemfu  7285  distrlem1prl  7291  distrlem1pru  7292  distrlem5prl  7295  distrlem5pru  7296  ltprordil  7298  ltexprlemfl  7318  ltexprlemrl  7319  ltexprlemfu  7320  ltexprlemru  7321  addcanprleml  7323  addcanprlemu  7324  recexprlem1ssl  7342  recexprlem1ssu  7343  recexprlemss1l  7344  recexprlemss1u  7345  aptiprleml  7348  aptiprlemu  7349  cauappcvgprlemladdfu  7363  cauappcvgprlemladdfl  7364  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  caucvgprlemladdfu  7386  caucvgprlemladdrl  7387  peano5uzti  9011  uzss  9196  ixxdisj  9527  ixxss1  9528  ixxss2  9529  ixxss12  9530  iocssre  9577  icossre  9578  iccssre  9579  icodisj  9616  fzss1  9684  fzss2  9685  fzoss1  9789  fzosplit  9795  fzouzsplit  9797  ssfzo12bi  9843  frecuzrdgtcl  10026  frecuzrdgdomlem  10031  ovshftex  10432  summodclem2a  10989  fsum3cvg3  11004  fsum2dlemstep  11042  phimullem  11693  ennnfonelemdm  11725  bastg  12012  tgss  12014  tgtop  12019  tgidm  12025  neisspw  12099  topssnei  12113  tgrest  12120  ssrest  12133  cnss1  12176  cnss2  12177  cnsscnp  12179  cnrest2r  12187  txdis  12227  xblss2ps  12332  xblss2  12333  cncfss  12483  dvfgg  12530