Theorem ssrdv 3230

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 1920	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3212	. 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 1393   e. wcel 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqelssd  3243  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  eq0rdv  3536  uniss  3909  intss1  3938  intmin  3943  intssunim  3945  iunss1  3976  iinss1  3977  ss2iun  3980  ssiun  4007  ssiun2  4008  iinss  4017  iinss2  4018  exmidundif  4290  exmidundifim  4291  sspwb  4302  tron  4473  ssorduni  4579  ordsson  4584  ordpwsucss  4659  xpsspw  4831  relop  4872  dmss  4922  dmcosseq  4996  ssrnres  5171  chfnrn  5748  ffnfv  5795  f1imass  5904  fo1stresm  6313  fo2ndresm  6314  oprssdmm  6323  fo2ndf  6379  reldmtpos  6405  smoiun  6453  tfrlemi14d  6485  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemres  6514  dcdifsnid  6658  qsss  6749  pmss12g  6830  mapss  6846  ixpssmap2g  6882  ixpssmapg  6883  en2eqpr  7080  exmidpw  7081  exmidpweq  7082  onunsnss  7090  undifdcss  7096  ssfii  7152  fiss  7155  difinfsn  7278  addnqprlemrl  7755  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  mulnqprlemrl  7771  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  distrlem1prl  7780  distrlem1pru  7781  distrlem5prl  7784  distrlem5pru  7785  ltprordil  7787  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  aptiprleml  7837  aptiprlemu  7838  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  suplocexprlemss  7913  suplocexprlemex  7920  peano5uzti  9566  uzss  9755  ixxdisj  10111  ixxss1  10112  ixxss2  10113  ixxss12  10114  iocssre  10161  icossre  10162  iccssre  10163  icodisj  10200  fzss1  10271  fzss2  10272  fzoss1  10381  fzosplit  10387  fzouzsplit  10389  ssfzo12bi  10443  frecuzrdgtcl  10646  frecuzrdgdomlem  10651  sswrd  11093  ovshftex  11346  summodclem2a  11908  fsum3cvg3  11923  fsum2dlemstep  11961  prodmodclem2a  12103  fprod2dlemstep  12149  bitsfzo  12482  phimullem  12763  1arith  12906  ennnfonelemdm  13007  trivsubgsnd  13754  ssnmz  13764  trivnsgd  13770  kerf1ghm  13827  conjnmz  13832  unitssd  14089  subrguss  14216  unitrrg  14247  lsssssubg  14358  lssintclm  14364  zsssubrg  14565  mulgrhm2  14590  znrrg  14640  psrbaglesuppg  14652  bastg  14751  tgss  14753  tgtop  14758  tgidm  14764  neisspw  14838  topssnei  14852  tgrest  14859  ssrest  14872  cnss1  14916  cnss2  14917  cnsscnp  14919  cnrest2r  14927  txdis  14967  xblss2ps  15094  xblss2  15095  xmettxlem  15199  xmettx  15200  cncfss  15273  cnopnap  15301  dvfgg  15378  dvcj  15399  usgruspgrben  16000