Theorem ssrdv 3161

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 1874	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		dfss2 3144	. 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 1351   e. wcel 2148   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  eqelssd  3174  sscon  3269  ssdif  3270  unss1  3304  ssrin  3360  eq0rdv  3467  uniss  3829  intss1  3858  intmin  3863  intssunim  3865  iunss1  3896  iinss1  3897  ss2iun  3900  ssiun  3927  ssiun2  3928  iinss  3936  iinss2  3937  exmidundif  4204  exmidundifim  4205  sspwb  4214  tron  4380  ssorduni  4484  ordsson  4489  ordpwsucss  4564  xpsspw  4736  relop  4774  dmss  4823  dmcosseq  4895  ssrnres  5068  chfnrn  5624  ffnfv  5671  f1imass  5770  fo1stresm  6157  fo2ndresm  6158  oprssdmm  6167  fo2ndf  6223  reldmtpos  6249  smoiun  6297  tfrlemi14d  6329  tfr1onlemres  6345  tfri1dALT  6347  tfrcllemres  6358  dcdifsnid  6500  qsss  6589  pmss12g  6670  mapss  6686  ixpssmap2g  6722  ixpssmapg  6723  en2eqpr  6902  exmidpw  6903  exmidpweq  6904  onunsnss  6911  undifdcss  6917  ssfii  6968  fiss  6971  difinfsn  7094  addnqprlemrl  7551  addnqprlemru  7552  addnqprlemfl  7553  addnqprlemfu  7554  mulnqprlemrl  7567  mulnqprlemru  7568  mulnqprlemfl  7569  mulnqprlemfu  7570  distrlem1prl  7576  distrlem1pru  7577  distrlem5prl  7580  distrlem5pru  7581  ltprordil  7583  ltexprlemfl  7603  ltexprlemrl  7604  ltexprlemfu  7605  ltexprlemru  7606  addcanprleml  7608  addcanprlemu  7609  recexprlem1ssl  7627  recexprlem1ssu  7628  recexprlemss1l  7629  recexprlemss1u  7630  aptiprleml  7633  aptiprlemu  7634  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  caucvgprlemladdfu  7671  caucvgprlemladdrl  7672  suplocexprlemss  7709  suplocexprlemex  7716  peano5uzti  9355  uzss  9542  ixxdisj  9897  ixxss1  9898  ixxss2  9899  ixxss12  9900  iocssre  9947  icossre  9948  iccssre  9949  icodisj  9986  fzss1  10056  fzss2  10057  fzoss1  10164  fzosplit  10170  fzouzsplit  10172  ssfzo12bi  10218  frecuzrdgtcl  10405  frecuzrdgdomlem  10410  ovshftex  10819  summodclem2a  11380  fsum3cvg3  11395  fsum2dlemstep  11433  prodmodclem2a  11575  fprod2dlemstep  11621  phimullem  12215  1arith  12355  ennnfonelemdm  12411  trivsubgsnd  12987  unitssd  13177  bastg  13343  tgss  13345  tgtop  13350  tgidm  13356  neisspw  13430  topssnei  13444  tgrest  13451  ssrest  13464  cnss1  13508  cnss2  13509  cnsscnp  13511  cnrest2r  13519  txdis  13559  xblss2ps  13686  xblss2  13687  xmettxlem  13791  xmettx  13792  cncfss  13852  cnopnap  13876  dvfgg  13939  dvcj  13955