Theorem ssrdv 3254

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 1927	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3235	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4	2, 3	sylibr 134	1 |- ( ph -> A C_ B )

This proof depends on syntax axioms:   -> wi 4   A.wal 1400   e. wcel 2209   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  eqelssd  3267  sscon  3363  ssdif  3364  unss1  3398  ssrin  3456  eq0rdv  3571  sspw  3702  uniss  3956  intss1  3985  intmin  3990  intssunim  3992  iunss1  4023  iinss1  4024  ss2iun  4027  ssiun  4054  ssiun2  4055  iinss  4064  iinss2  4065  exmidundif  4343  exmidundifim  4344  sspwb  4356  tron  4527  ssorduni  4634  ordsson  4639  ordpwsucss  4714  xpsspw  4887  relop  4930  dmss  4980  dmcosseq  5054  ssrnres  5230  chfnrn  5820  ffnfv  5866  f1imass  5980  abrexss  6358  fo1stresm  6395  fo2ndresm  6396  oprssdmm  6405  fo2ndf  6463  funsssuppss  6498  suppssdc  6500  suppssfvg  6503  reldmtpos  6524  smoiun  6572  tfrlemi14d  6604  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemres  6633  dcdifsnid  6777  qsss  6868  pmss12g  6956  mapss  6973  ixpssmap2g  7009  ixpssmapg  7010  en2eqpr  7214  exmidpw  7215  exmidpweq  7216  onunsnss  7224  undifdcss  7230  ssfii  7308  fiss  7311  difinfsn  7440  addnqprlemrl  7924  addnqprlemru  7925  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemrl  7940  mulnqprlemru  7941  mulnqprlemfl  7942  mulnqprlemfu  7943  distrlem1prl  7949  distrlem1pru  7950  distrlem5prl  7953  distrlem5pru  7954  ltprordil  7956  ltexprlemfl  7976  ltexprlemrl  7977  ltexprlemfu  7978  ltexprlemru  7979  addcanprleml  7981  addcanprlemu  7982  recexprlem1ssl  8000  recexprlem1ssu  8001  recexprlemss1l  8002  recexprlemss1u  8003  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  suplocexprlemss  8082  suplocexprlemex  8089  peano5uzti  9758  uzss  9952  ixxdisj  10315  ixxss1  10316  ixxss2  10317  ixxss12  10318  iocssre  10365  icossre  10366  iccssre  10367  icodisj  10404  fzss1  10479  fzss2  10480  fzoss1  10590  fzosplit  10596  fzouzsplit  10598  ssfzo12bi  10653  frecuzrdgtcl  10862  frecuzrdgdomlem  10867  sswrd  11327  ovshftex  11598  summodclem2a  12164  fsum3cvg3  12179  fsum2dlemstep  12217  prodmodclem2a  12359  fprod2dlemstep  12405  bitsfzo  12738  phimullem  13023  1arith  13166  ennnfonelemdm  13360  trivsubgsnd  14053  ssnmz  14063  trivnsgd  14069  kerf1ghm  14126  conjnmz  14131  unitssd  14465  subrguss  14593  unitrrg  14625  lsssssubg  14764  lssintclm  14770  zsssubrg  14971  mulgrhm2  14994  znrrg  15044  psrbaglesuppg  15106  bastg  15211  tgss  15213  tgtop  15218  tgidm  15224  neisspw  15298  topssnei  15312  tgrest  15319  ssrest  15332  cnss1  15376  cnss2  15377  cnsscnp  15379  cnrest2r  15387  txdis  15427  xblss2ps  15554  xblss2  15555  xmettxlem  15659  xmettx  15660  cncfss  15733  cnopnap  15761  dvfgg  15838  dvcj  15859  ppiqsval  16156  ppinprm  16171  usgruspgrben  16525  uhgrissubgr  16600  uhgrspansubgrlem  16615