Theorem ssrdv 3208

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 1898	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3190	. 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 2178   C_ wss 3175

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3181  df-ss 3188

This theorem is referenced by:  eqelssd  3221  sscon  3316  ssdif  3317  unss1  3351  ssrin  3407  eq0rdv  3514  uniss  3886  intss1  3915  intmin  3920  intssunim  3922  iunss1  3953  iinss1  3954  ss2iun  3957  ssiun  3984  ssiun2  3985  iinss  3994  iinss2  3995  exmidundif  4267  exmidundifim  4268  sspwb  4279  tron  4448  ssorduni  4554  ordsson  4559  ordpwsucss  4634  xpsspw  4806  relop  4847  dmss  4897  dmcosseq  4970  ssrnres  5145  chfnrn  5716  ffnfv  5763  f1imass  5868  fo1stresm  6272  fo2ndresm  6273  oprssdmm  6282  fo2ndf  6338  reldmtpos  6364  smoiun  6412  tfrlemi14d  6444  tfr1onlemres  6460  tfri1dALT  6462  tfrcllemres  6473  dcdifsnid  6615  qsss  6706  pmss12g  6787  mapss  6803  ixpssmap2g  6839  ixpssmapg  6840  en2eqpr  7032  exmidpw  7033  exmidpweq  7034  onunsnss  7042  undifdcss  7048  ssfii  7104  fiss  7107  difinfsn  7230  addnqprlemrl  7707  addnqprlemru  7708  addnqprlemfl  7709  addnqprlemfu  7710  mulnqprlemrl  7723  mulnqprlemru  7724  mulnqprlemfl  7725  mulnqprlemfu  7726  distrlem1prl  7732  distrlem1pru  7733  distrlem5prl  7736  distrlem5pru  7737  ltprordil  7739  ltexprlemfl  7759  ltexprlemrl  7760  ltexprlemfu  7761  ltexprlemru  7762  addcanprleml  7764  addcanprlemu  7765  recexprlem1ssl  7783  recexprlem1ssu  7784  recexprlemss1l  7785  recexprlemss1u  7786  aptiprleml  7789  aptiprlemu  7790  cauappcvgprlemladdfu  7804  cauappcvgprlemladdfl  7805  cauappcvgprlemladdru  7806  cauappcvgprlemladdrl  7807  caucvgprlemladdfu  7827  caucvgprlemladdrl  7828  suplocexprlemss  7865  suplocexprlemex  7872  peano5uzti  9518  uzss  9706  ixxdisj  10062  ixxss1  10063  ixxss2  10064  ixxss12  10065  iocssre  10112  icossre  10113  iccssre  10114  icodisj  10151  fzss1  10222  fzss2  10223  fzoss1  10332  fzosplit  10338  fzouzsplit  10340  ssfzo12bi  10393  frecuzrdgtcl  10596  frecuzrdgdomlem  10601  sswrd  11042  ovshftex  11291  summodclem2a  11853  fsum3cvg3  11868  fsum2dlemstep  11906  prodmodclem2a  12048  fprod2dlemstep  12094  bitsfzo  12427  phimullem  12708  1arith  12851  ennnfonelemdm  12952  trivsubgsnd  13698  ssnmz  13708  trivnsgd  13714  kerf1ghm  13771  conjnmz  13776  unitssd  14032  subrguss  14159  unitrrg  14190  lsssssubg  14301  lssintclm  14307  zsssubrg  14508  mulgrhm2  14533  znrrg  14583  psrbaglesuppg  14595  bastg  14694  tgss  14696  tgtop  14701  tgidm  14707  neisspw  14781  topssnei  14795  tgrest  14802  ssrest  14815  cnss1  14859  cnss2  14860  cnsscnp  14862  cnrest2r  14870  txdis  14910  xblss2ps  15037  xblss2  15038  xmettxlem  15142  xmettx  15143  cncfss  15216  cnopnap  15244  dvfgg  15321  dvcj  15342  usgruspgrben  15941