Theorem ssrdv 3176

Description: Deduction based on subclass definition. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
ssrdv.1	⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))

Assertion

Ref	Expression
ssrdv	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Proof of Theorem ssrdv

Step	Hyp	Ref	Expression
1		ssrdv.1	. . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	alrimiv 1885	. 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
3		dfss2 3159	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
4	2, 3	sylibr 134	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Syntax hints:   → wi 4  ∀wal 1362   ∈ wcel 2160   ⊆ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  eqelssd  3189  sscon  3284  ssdif  3285  unss1  3319  ssrin  3375  eq0rdv  3482  uniss  3845  intss1  3874  intmin  3879  intssunim  3881  iunss1  3912  iinss1  3913  ss2iun  3916  ssiun  3943  ssiun2  3944  iinss  3953  iinss2  3954  exmidundif  4224  exmidundifim  4225  sspwb  4234  tron  4400  ssorduni  4504  ordsson  4509  ordpwsucss  4584  xpsspw  4756  relop  4795  dmss  4844  dmcosseq  4916  ssrnres  5089  chfnrn  5648  ffnfv  5695  f1imass  5796  fo1stresm  6186  fo2ndresm  6187  oprssdmm  6196  fo2ndf  6252  reldmtpos  6278  smoiun  6326  tfrlemi14d  6358  tfr1onlemres  6374  tfri1dALT  6376  tfrcllemres  6387  dcdifsnid  6529  qsss  6620  pmss12g  6701  mapss  6717  ixpssmap2g  6753  ixpssmapg  6754  en2eqpr  6935  exmidpw  6936  exmidpweq  6937  onunsnss  6945  undifdcss  6951  ssfii  7003  fiss  7006  difinfsn  7129  addnqprlemrl  7586  addnqprlemru  7587  addnqprlemfl  7588  addnqprlemfu  7589  mulnqprlemrl  7602  mulnqprlemru  7603  mulnqprlemfl  7604  mulnqprlemfu  7605  distrlem1prl  7611  distrlem1pru  7612  distrlem5prl  7615  distrlem5pru  7616  ltprordil  7618  ltexprlemfl  7638  ltexprlemrl  7639  ltexprlemfu  7640  ltexprlemru  7641  addcanprleml  7643  addcanprlemu  7644  recexprlem1ssl  7662  recexprlem1ssu  7663  recexprlemss1l  7664  recexprlemss1u  7665  aptiprleml  7668  aptiprlemu  7669  cauappcvgprlemladdfu  7683  cauappcvgprlemladdfl  7684  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  caucvgprlemladdfu  7706  caucvgprlemladdrl  7707  suplocexprlemss  7744  suplocexprlemex  7751  peano5uzti  9391  uzss  9578  ixxdisj  9933  ixxss1  9934  ixxss2  9935  ixxss12  9936  iocssre  9983  icossre  9984  iccssre  9985  icodisj  10022  fzss1  10093  fzss2  10094  fzoss1  10201  fzosplit  10207  fzouzsplit  10209  ssfzo12bi  10255  frecuzrdgtcl  10443  frecuzrdgdomlem  10448  ovshftex  10860  summodclem2a  11421  fsum3cvg3  11436  fsum2dlemstep  11474  prodmodclem2a  11616  fprod2dlemstep  11662  phimullem  12257  1arith  12399  ennnfonelemdm  12471  trivsubgsnd  13140  ssnmz  13150  trivnsgd  13156  kerf1ghm  13213  conjnmz  13218  unitssd  13459  subrguss  13583  lsssssubg  13694  lssintclm  13700  zsssubrg  13888  mulgrhm2  13908  psrbaglesuppg  13950  bastg  14018  tgss  14020  tgtop  14025  tgidm  14031  neisspw  14105  topssnei  14119  tgrest  14126  ssrest  14139  cnss1  14183  cnss2  14184  cnsscnp  14186  cnrest2r  14194  txdis  14234  xblss2ps  14361  xblss2  14362  xmettxlem  14466  xmettx  14467  cncfss  14527  cnopnap  14551  dvfgg  14614  dvcj  14630