Theorem ssrdv 3199

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 1897	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3181	. 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 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqelssd  3212  sscon  3307  ssdif  3308  unss1  3342  ssrin  3398  eq0rdv  3505  uniss  3871  intss1  3900  intmin  3905  intssunim  3907  iunss1  3938  iinss1  3939  ss2iun  3942  ssiun  3969  ssiun2  3970  iinss  3979  iinss2  3980  exmidundif  4250  exmidundifim  4251  sspwb  4260  tron  4429  ssorduni  4535  ordsson  4540  ordpwsucss  4615  xpsspw  4787  relop  4828  dmss  4877  dmcosseq  4950  ssrnres  5125  chfnrn  5691  ffnfv  5738  f1imass  5843  fo1stresm  6247  fo2ndresm  6248  oprssdmm  6257  fo2ndf  6313  reldmtpos  6339  smoiun  6387  tfrlemi14d  6419  tfr1onlemres  6435  tfri1dALT  6437  tfrcllemres  6448  dcdifsnid  6590  qsss  6681  pmss12g  6762  mapss  6778  ixpssmap2g  6814  ixpssmapg  6815  en2eqpr  7004  exmidpw  7005  exmidpweq  7006  onunsnss  7014  undifdcss  7020  ssfii  7076  fiss  7079  difinfsn  7202  addnqprlemrl  7670  addnqprlemru  7671  addnqprlemfl  7672  addnqprlemfu  7673  mulnqprlemrl  7686  mulnqprlemru  7687  mulnqprlemfl  7688  mulnqprlemfu  7689  distrlem1prl  7695  distrlem1pru  7696  distrlem5prl  7699  distrlem5pru  7700  ltprordil  7702  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  aptiprleml  7752  aptiprlemu  7753  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  suplocexprlemss  7828  suplocexprlemex  7835  peano5uzti  9481  uzss  9669  ixxdisj  10025  ixxss1  10026  ixxss2  10027  ixxss12  10028  iocssre  10075  icossre  10076  iccssre  10077  icodisj  10114  fzss1  10185  fzss2  10186  fzoss1  10295  fzosplit  10301  fzouzsplit  10303  ssfzo12bi  10354  frecuzrdgtcl  10557  frecuzrdgdomlem  10562  sswrd  11003  ovshftex  11130  summodclem2a  11692  fsum3cvg3  11707  fsum2dlemstep  11745  prodmodclem2a  11887  fprod2dlemstep  11933  bitsfzo  12266  phimullem  12547  1arith  12690  ennnfonelemdm  12791  trivsubgsnd  13537  ssnmz  13547  trivnsgd  13553  kerf1ghm  13610  conjnmz  13615  unitssd  13871  subrguss  13998  unitrrg  14029  lsssssubg  14140  lssintclm  14146  zsssubrg  14347  mulgrhm2  14372  znrrg  14422  psrbaglesuppg  14434  bastg  14533  tgss  14535  tgtop  14540  tgidm  14546  neisspw  14620  topssnei  14634  tgrest  14641  ssrest  14654  cnss1  14698  cnss2  14699  cnsscnp  14701  cnrest2r  14709  txdis  14749  xblss2ps  14876  xblss2  14877  xmettxlem  14981  xmettx  14982  cncfss  15055  cnopnap  15083  dvfgg  15160  dvcj  15181