Theorem ssrdv 3162

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 3145	. 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 3130

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 3136  df-ss 3143

This theorem is referenced by:  eqelssd  3175  sscon  3270  ssdif  3271  unss1  3305  ssrin  3361  eq0rdv  3468  uniss  3831  intss1  3860  intmin  3865  intssunim  3867  iunss1  3898  iinss1  3899  ss2iun  3902  ssiun  3929  ssiun2  3930  iinss  3939  iinss2  3940  exmidundif  4207  exmidundifim  4208  sspwb  4217  tron  4383  ssorduni  4487  ordsson  4492  ordpwsucss  4567  xpsspw  4739  relop  4778  dmss  4827  dmcosseq  4899  ssrnres  5072  chfnrn  5628  ffnfv  5675  f1imass  5775  fo1stresm  6162  fo2ndresm  6163  oprssdmm  6172  fo2ndf  6228  reldmtpos  6254  smoiun  6302  tfrlemi14d  6334  tfr1onlemres  6350  tfri1dALT  6352  tfrcllemres  6363  dcdifsnid  6505  qsss  6594  pmss12g  6675  mapss  6691  ixpssmap2g  6727  ixpssmapg  6728  en2eqpr  6907  exmidpw  6908  exmidpweq  6909  onunsnss  6916  undifdcss  6922  ssfii  6973  fiss  6976  difinfsn  7099  addnqprlemrl  7556  addnqprlemru  7557  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemrl  7572  mulnqprlemru  7573  mulnqprlemfl  7574  mulnqprlemfu  7575  distrlem1prl  7581  distrlem1pru  7582  distrlem5prl  7585  distrlem5pru  7586  ltprordil  7588  ltexprlemfl  7608  ltexprlemrl  7609  ltexprlemfu  7610  ltexprlemru  7611  addcanprleml  7613  addcanprlemu  7614  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  recexprlemss1u  7635  aptiprleml  7638  aptiprlemu  7639  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  suplocexprlemss  7714  suplocexprlemex  7721  peano5uzti  9361  uzss  9548  ixxdisj  9903  ixxss1  9904  ixxss2  9905  ixxss12  9906  iocssre  9953  icossre  9954  iccssre  9955  icodisj  9992  fzss1  10063  fzss2  10064  fzoss1  10171  fzosplit  10177  fzouzsplit  10179  ssfzo12bi  10225  frecuzrdgtcl  10412  frecuzrdgdomlem  10417  ovshftex  10828  summodclem2a  11389  fsum3cvg3  11404  fsum2dlemstep  11442  prodmodclem2a  11584  fprod2dlemstep  11630  phimullem  12225  1arith  12365  ennnfonelemdm  12421  trivsubgsnd  13061  ssnmz  13071  trivnsgd  13077  unitssd  13278  subrguss  13357  zsssubrg  13482  bastg  13564  tgss  13566  tgtop  13571  tgidm  13577  neisspw  13651  topssnei  13665  tgrest  13672  ssrest  13685  cnss1  13729  cnss2  13730  cnsscnp  13732  cnrest2r  13740  txdis  13780  xblss2ps  13907  xblss2  13908  xmettxlem  14012  xmettx  14013  cncfss  14073  cnopnap  14097  dvfgg  14160  dvcj  14176