Theorem ssrdv 3207

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 1898	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3189	. 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 1371   e. wcel 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  eqelssd  3220  sscon  3315  ssdif  3316  unss1  3350  ssrin  3406  eq0rdv  3513  uniss  3885  intss1  3914  intmin  3919  intssunim  3921  iunss1  3952  iinss1  3953  ss2iun  3956  ssiun  3983  ssiun2  3984  iinss  3993  iinss2  3994  exmidundif  4266  exmidundifim  4267  sspwb  4278  tron  4447  ssorduni  4553  ordsson  4558  ordpwsucss  4633  xpsspw  4805  relop  4846  dmss  4896  dmcosseq  4969  ssrnres  5144  chfnrn  5714  ffnfv  5761  f1imass  5866  fo1stresm  6270  fo2ndresm  6271  oprssdmm  6280  fo2ndf  6336  reldmtpos  6362  smoiun  6410  tfrlemi14d  6442  tfr1onlemres  6458  tfri1dALT  6460  tfrcllemres  6471  dcdifsnid  6613  qsss  6704  pmss12g  6785  mapss  6801  ixpssmap2g  6837  ixpssmapg  6838  en2eqpr  7030  exmidpw  7031  exmidpweq  7032  onunsnss  7040  undifdcss  7046  ssfii  7102  fiss  7105  difinfsn  7228  addnqprlemrl  7705  addnqprlemru  7706  addnqprlemfl  7707  addnqprlemfu  7708  mulnqprlemrl  7721  mulnqprlemru  7722  mulnqprlemfl  7723  mulnqprlemfu  7724  distrlem1prl  7730  distrlem1pru  7731  distrlem5prl  7734  distrlem5pru  7735  ltprordil  7737  ltexprlemfl  7757  ltexprlemrl  7758  ltexprlemfu  7759  ltexprlemru  7760  addcanprleml  7762  addcanprlemu  7763  recexprlem1ssl  7781  recexprlem1ssu  7782  recexprlemss1l  7783  recexprlemss1u  7784  aptiprleml  7787  aptiprlemu  7788  cauappcvgprlemladdfu  7802  cauappcvgprlemladdfl  7803  cauappcvgprlemladdru  7804  cauappcvgprlemladdrl  7805  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  suplocexprlemss  7863  suplocexprlemex  7870  peano5uzti  9516  uzss  9704  ixxdisj  10060  ixxss1  10061  ixxss2  10062  ixxss12  10063  iocssre  10110  icossre  10111  iccssre  10112  icodisj  10149  fzss1  10220  fzss2  10221  fzoss1  10330  fzosplit  10336  fzouzsplit  10338  ssfzo12bi  10391  frecuzrdgtcl  10594  frecuzrdgdomlem  10599  sswrd  11040  ovshftex  11245  summodclem2a  11807  fsum3cvg3  11822  fsum2dlemstep  11860  prodmodclem2a  12002  fprod2dlemstep  12048  bitsfzo  12381  phimullem  12662  1arith  12805  ennnfonelemdm  12906  trivsubgsnd  13652  ssnmz  13662  trivnsgd  13668  kerf1ghm  13725  conjnmz  13730  unitssd  13986  subrguss  14113  unitrrg  14144  lsssssubg  14255  lssintclm  14261  zsssubrg  14462  mulgrhm2  14487  znrrg  14537  psrbaglesuppg  14549  bastg  14648  tgss  14650  tgtop  14655  tgidm  14661  neisspw  14735  topssnei  14749  tgrest  14756  ssrest  14769  cnss1  14813  cnss2  14814  cnsscnp  14816  cnrest2r  14824  txdis  14864  xblss2ps  14991  xblss2  14992  xmettxlem  15096  xmettx  15097  cncfss  15170  cnopnap  15198  dvfgg  15275  dvcj  15296