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  6529  smoiun  6577  tfrlemi14d  6609  tfr1onlemres  6625  tfri1dALT  6627  tfrcllemres  6638  dcdifsnid  6782  qsss  6873  pmss12g  6961  mapss  6979  ixpssmap2g  7015  ixpssmapg  7016  en2eqpr  7220  exmidpw  7221  exmidpweq  7222  onunsnss  7230  undifdcss  7236  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  9764  uzss  9958  ixxdisj  10321  ixxss1  10322  ixxss2  10323  ixxss12  10324  iocssre  10371  icossre  10372  iccssre  10373  icodisj  10410  fzss1  10485  fzss2  10486  fzoss1  10596  fzosplit  10602  fzouzsplit  10604  ssfzo12bi  10659  frecuzrdgtcl  10869  frecuzrdgdomlem  10874  sswrd  11334  ovshftex  11605  summodclem2a  12172  fsum3cvg3  12187  fsum2dlemstep  12225  prodmodclem2a  12367  fprod2dlemstep  12413  bitsfzo  12746  phimullem  13031  1arith  13174  ennnfonelemdm  13368  trivsubgsnd  14062  ssnmz  14072  trivnsgd  14078  kerf1ghm  14135  conjnmz  14140  gsum2d2fi  14273  unitssd  14524  subrguss  14652  unitrrg  14684  lsssssubg  14823  lssintclm  14829  zsssubrg  15030  mulgrhm2  15053  znrrg  15103  psrbaglesuppg  15170  psrbaglefifi  15175  psrbagmaxlem1x  15181  psrbagmaxlem1y  15182  mvrclfi  15226  mplsubgfilemcl  15232  bastg  15304  tgss  15306  tgtop  15311  tgidm  15317  neisspw  15391  topssnei  15405  tgrest  15412  ssrest  15425  cnss1  15469  cnss2  15470  cnsscnp  15472  cnrest2r  15480  txdis  15520  xblss2ps  15647  xblss2  15648  xmettxlem  15752  xmettx  15753  cncfss  15826  cnopnap  15854  dvfgg  15931  dvcj  15952  ppiqsval  16257  ppinprm  16277  chtnprm  16279  usgruspgrben  16649  uhgrissubgr  16724  uhgrspansubgrlem  16739