Theorem ssrdv 3190

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		ssalel 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  3203  sscon  3298  ssdif  3299  unss1  3333  ssrin  3389  eq0rdv  3496  uniss  3861  intss1  3890  intmin  3895  intssunim  3897  iunss1  3928  iinss1  3929  ss2iun  3932  ssiun  3959  ssiun2  3960  iinss  3969  iinss2  3970  exmidundif  4240  exmidundifim  4241  sspwb  4250  tron  4418  ssorduni  4524  ordsson  4529  ordpwsucss  4604  xpsspw  4776  relop  4817  dmss  4866  dmcosseq  4938  ssrnres  5113  chfnrn  5676  ffnfv  5723  f1imass  5824  fo1stresm  6228  fo2ndresm  6229  oprssdmm  6238  fo2ndf  6294  reldmtpos  6320  smoiun  6368  tfrlemi14d  6400  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemres  6429  dcdifsnid  6571  qsss  6662  pmss12g  6743  mapss  6759  ixpssmap2g  6795  ixpssmapg  6796  en2eqpr  6977  exmidpw  6978  exmidpweq  6979  onunsnss  6987  undifdcss  6993  ssfii  7049  fiss  7052  difinfsn  7175  addnqprlemrl  7641  addnqprlemru  7642  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemrl  7657  mulnqprlemru  7658  mulnqprlemfl  7659  mulnqprlemfu  7660  distrlem1prl  7666  distrlem1pru  7667  distrlem5prl  7670  distrlem5pru  7671  ltprordil  7673  ltexprlemfl  7693  ltexprlemrl  7694  ltexprlemfu  7695  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  recexprlem1ssl  7717  recexprlem1ssu  7718  recexprlemss1l  7719  recexprlemss1u  7720  aptiprleml  7723  aptiprlemu  7724  cauappcvgprlemladdfu  7738  cauappcvgprlemladdfl  7739  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  suplocexprlemss  7799  suplocexprlemex  7806  peano5uzti  9451  uzss  9639  ixxdisj  9995  ixxss1  9996  ixxss2  9997  ixxss12  9998  iocssre  10045  icossre  10046  iccssre  10047  icodisj  10084  fzss1  10155  fzss2  10156  fzoss1  10264  fzosplit  10270  fzouzsplit  10272  ssfzo12bi  10318  frecuzrdgtcl  10521  frecuzrdgdomlem  10526  sswrd  10961  ovshftex  11001  summodclem2a  11563  fsum3cvg3  11578  fsum2dlemstep  11616  prodmodclem2a  11758  fprod2dlemstep  11804  bitsfzo  12137  phimullem  12418  1arith  12561  ennnfonelemdm  12662  trivsubgsnd  13407  ssnmz  13417  trivnsgd  13423  kerf1ghm  13480  conjnmz  13485  unitssd  13741  subrguss  13868  unitrrg  13899  lsssssubg  14010  lssintclm  14016  zsssubrg  14217  mulgrhm2  14242  znrrg  14292  psrbaglesuppg  14302  bastg  14381  tgss  14383  tgtop  14388  tgidm  14394  neisspw  14468  topssnei  14482  tgrest  14489  ssrest  14502  cnss1  14546  cnss2  14547  cnsscnp  14549  cnrest2r  14557  txdis  14597  xblss2ps  14724  xblss2  14725  xmettxlem  14829  xmettx  14830  cncfss  14903  cnopnap  14931  dvfgg  15008  dvcj  15029