Theorem ssrdv 3189

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 1888	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3172	. 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 1362   e. wcel 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  eqelssd  3202  sscon  3297  ssdif  3298  unss1  3332  ssrin  3388  eq0rdv  3495  uniss  3860  intss1  3889  intmin  3894  intssunim  3896  iunss1  3927  iinss1  3928  ss2iun  3931  ssiun  3958  ssiun2  3959  iinss  3968  iinss2  3969  exmidundif  4239  exmidundifim  4240  sspwb  4249  tron  4417  ssorduni  4523  ordsson  4528  ordpwsucss  4603  xpsspw  4775  relop  4816  dmss  4865  dmcosseq  4937  ssrnres  5112  chfnrn  5673  ffnfv  5720  f1imass  5821  fo1stresm  6219  fo2ndresm  6220  oprssdmm  6229  fo2ndf  6285  reldmtpos  6311  smoiun  6359  tfrlemi14d  6391  tfr1onlemres  6407  tfri1dALT  6409  tfrcllemres  6420  dcdifsnid  6562  qsss  6653  pmss12g  6734  mapss  6750  ixpssmap2g  6786  ixpssmapg  6787  en2eqpr  6968  exmidpw  6969  exmidpweq  6970  onunsnss  6978  undifdcss  6984  ssfii  7040  fiss  7043  difinfsn  7166  addnqprlemrl  7624  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemrl  7640  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  distrlem1prl  7649  distrlem1pru  7650  distrlem5prl  7653  distrlem5pru  7654  ltprordil  7656  ltexprlemfl  7676  ltexprlemrl  7677  ltexprlemfu  7678  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  aptiprleml  7706  aptiprlemu  7707  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  suplocexprlemss  7782  suplocexprlemex  7789  peano5uzti  9434  uzss  9622  ixxdisj  9978  ixxss1  9979  ixxss2  9980  ixxss12  9981  iocssre  10028  icossre  10029  iccssre  10030  icodisj  10067  fzss1  10138  fzss2  10139  fzoss1  10247  fzosplit  10253  fzouzsplit  10255  ssfzo12bi  10301  frecuzrdgtcl  10504  frecuzrdgdomlem  10509  sswrd  10944  ovshftex  10984  summodclem2a  11546  fsum3cvg3  11561  fsum2dlemstep  11599  prodmodclem2a  11741  fprod2dlemstep  11787  bitsfzo  12119  phimullem  12393  1arith  12536  ennnfonelemdm  12637  trivsubgsnd  13331  ssnmz  13341  trivnsgd  13347  kerf1ghm  13404  conjnmz  13409  unitssd  13665  subrguss  13792  unitrrg  13823  lsssssubg  13934  lssintclm  13940  zsssubrg  14141  mulgrhm2  14166  znrrg  14216  psrbaglesuppg  14226  bastg  14297  tgss  14299  tgtop  14304  tgidm  14310  neisspw  14384  topssnei  14398  tgrest  14405  ssrest  14418  cnss1  14462  cnss2  14463  cnsscnp  14465  cnrest2r  14473  txdis  14513  xblss2ps  14640  xblss2  14641  xmettxlem  14745  xmettx  14746  cncfss  14819  cnopnap  14847  dvfgg  14924  dvcj  14945