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  4345  exmidundifim  4346  sspwb  4358  tron  4529  ssorduni  4636  ordsson  4641  ordpwsucss  4716  xpsspw  4889  relop  4932  dmss  4982  dmcosseq  5056  ssrnres  5233  chfnrn  5823  ffnfv  5869  f1imass  5983  abrexss  6362  fo1stresm  6399  fo2ndresm  6400  oprssdmm  6409  fo2ndf  6467  funsssuppss  6502  suppssdc  6504  suppssfvg  6507  reldmtpos  6528  smoiun  6576  tfrlemi14d  6608  tfr1onlemres  6624  tfri1dALT  6626  tfrcllemres  6637  dcdifsnid  6781  qsss  6872  pmss12g  6960  mapss  6977  ixpssmap2g  7013  ixpssmapg  7014  en2eqpr  7218  exmidpw  7219  exmidpweq  7220  onunsnss  7228  undifdcss  7234  ssfii  7313  fiss  7316  difinfsn  7446  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  distrlem1prl  7955  distrlem1pru  7956  distrlem5prl  7959  distrlem5pru  7960  ltprordil  7962  ltexprlemfl  7982  ltexprlemrl  7983  ltexprlemfu  7984  ltexprlemru  7985  addcanprleml  7987  addcanprlemu  7988  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  aptiprleml  8012  aptiprlemu  8013  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  suplocexprlemss  8088  suplocexprlemex  8095  peano5uzti  9765  uzss  9959  ixxdisj  10322  ixxss1  10323  ixxss2  10324  ixxss12  10325  iocssre  10372  icossre  10373  iccssre  10374  icodisj  10411  fzss1  10486  fzss2  10487  fzoss1  10597  fzosplit  10603  fzouzsplit  10605  ssfzo12bi  10660  frecuzrdgtcl  10870  frecuzrdgdomlem  10875  sswrd  11335  ovshftex  11606  summodclem2a  12173  fsum3cvg3  12188  fsum2dlemstep  12226  prodmodclem2a  12368  fprod2dlemstep  12414  bitsfzo  12747  phimullem  13032  1arith  13175  ennnfonelemdm  13369  trivsubgsnd  14063  ssnmz  14073  trivnsgd  14079  kerf1ghm  14136  conjnmz  14141  gsum2d2fi  14274  unitssd  14525  subrguss  14653  unitrrg  14685  lsssssubg  14824  lssintclm  14830  zsssubrg  15031  mulgrhm2  15054  znrrg  15104  psrbaglesuppg  15166  psrbaglefifi  15172  bastg  15287  tgss  15289  tgtop  15294  tgidm  15300  neisspw  15374  topssnei  15388  tgrest  15395  ssrest  15408  cnss1  15452  cnss2  15453  cnsscnp  15455  cnrest2r  15463  txdis  15503  xblss2ps  15630  xblss2  15631  xmettxlem  15735  xmettx  15736  cncfss  15809  cnopnap  15837  dvfgg  15914  dvcj  15935  ppiqsval  16240  ppinprm  16260  chtnprm  16262  usgruspgrben  16632  uhgrissubgr  16707  uhgrspansubgrlem  16722