Theorem ssrdv 3230

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 1920	. 2 |- ( ph -> A. x ( x e. A -> x e. B ) )
3		ssalel 3212	. 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 1393   e. wcel 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqelssd  3243  sscon  3338  ssdif  3339  unss1  3373  ssrin  3429  eq0rdv  3536  uniss  3909  intss1  3938  intmin  3943  intssunim  3945  iunss1  3976  iinss1  3977  ss2iun  3980  ssiun  4007  ssiun2  4008  iinss  4017  iinss2  4018  exmidundif  4290  exmidundifim  4291  sspwb  4302  tron  4473  ssorduni  4579  ordsson  4584  ordpwsucss  4659  xpsspw  4831  relop  4872  dmss  4922  dmcosseq  4996  ssrnres  5171  chfnrn  5746  ffnfv  5793  f1imass  5898  fo1stresm  6307  fo2ndresm  6308  oprssdmm  6317  fo2ndf  6373  reldmtpos  6399  smoiun  6447  tfrlemi14d  6479  tfr1onlemres  6495  tfri1dALT  6497  tfrcllemres  6508  dcdifsnid  6650  qsss  6741  pmss12g  6822  mapss  6838  ixpssmap2g  6874  ixpssmapg  6875  en2eqpr  7069  exmidpw  7070  exmidpweq  7071  onunsnss  7079  undifdcss  7085  ssfii  7141  fiss  7144  difinfsn  7267  addnqprlemrl  7744  addnqprlemru  7745  addnqprlemfl  7746  addnqprlemfu  7747  mulnqprlemrl  7760  mulnqprlemru  7761  mulnqprlemfl  7762  mulnqprlemfu  7763  distrlem1prl  7769  distrlem1pru  7770  distrlem5prl  7773  distrlem5pru  7774  ltprordil  7776  ltexprlemfl  7796  ltexprlemrl  7797  ltexprlemfu  7798  ltexprlemru  7799  addcanprleml  7801  addcanprlemu  7802  recexprlem1ssl  7820  recexprlem1ssu  7821  recexprlemss1l  7822  recexprlemss1u  7823  aptiprleml  7826  aptiprlemu  7827  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  cauappcvgprlemladdru  7843  cauappcvgprlemladdrl  7844  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  suplocexprlemss  7902  suplocexprlemex  7909  peano5uzti  9555  uzss  9743  ixxdisj  10099  ixxss1  10100  ixxss2  10101  ixxss12  10102  iocssre  10149  icossre  10150  iccssre  10151  icodisj  10188  fzss1  10259  fzss2  10260  fzoss1  10369  fzosplit  10375  fzouzsplit  10377  ssfzo12bi  10431  frecuzrdgtcl  10634  frecuzrdgdomlem  10639  sswrd  11080  ovshftex  11330  summodclem2a  11892  fsum3cvg3  11907  fsum2dlemstep  11945  prodmodclem2a  12087  fprod2dlemstep  12133  bitsfzo  12466  phimullem  12747  1arith  12890  ennnfonelemdm  12991  trivsubgsnd  13738  ssnmz  13748  trivnsgd  13754  kerf1ghm  13811  conjnmz  13816  unitssd  14073  subrguss  14200  unitrrg  14231  lsssssubg  14342  lssintclm  14348  zsssubrg  14549  mulgrhm2  14574  znrrg  14624  psrbaglesuppg  14636  bastg  14735  tgss  14737  tgtop  14742  tgidm  14748  neisspw  14822  topssnei  14836  tgrest  14843  ssrest  14856  cnss1  14900  cnss2  14901  cnsscnp  14903  cnrest2r  14911  txdis  14951  xblss2ps  15078  xblss2  15079  xmettxlem  15183  xmettx  15184  cncfss  15257  cnopnap  15285  dvfgg  15362  dvcj  15383  usgruspgrben  15984