Theorem sseld 3921

Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sseld	⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem sseld

Step	Hyp	Ref	Expression
1		sseld.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssel 3916	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2812  df-ss 3907

This theorem is referenced by:  sselda  3922  sseldd  3923  ssneld  3924  eqrrabd  4027  elelpwi  4552  ssbrd  5129  uniopel  5464  exopxfr2  5793  dmrnssfld  5923  preddowncl  6290  opelf  6695  elfvunirn  6864  fimarab  6908  fvimacnv  6999  ffvelcdm  7027  fnsnr  7111  f1imass  7212  onminex  7749  xpord2pred  8088  extmptsuppeq  8131  suppssr  8138  suppssrg  8139  dftpos3  8187  oa00  8487  omordi  8494  omlimcl  8506  omeulem1  8510  nnmordi  8560  mapsnd  8827  ixpf  8861  pw2f1olem  9012  pssnn  9096  findcard3  9186  ixpfi2  9253  fissuni  9260  elfiun  9336  dffi3  9337  supssd  9369  infssd  9400  ordiso2  9423  ordtypelem7  9432  ixpiunwdom  9498  inf3lem2  9541  cantnfp1lem3  9592  cantnfp1  9593  cantnflem1  9601  cantnf  9605  trcl  9640  r1ordg  9693  rankelb  9739  rankuni2b  9768  rankval4  9782  tcrank  9799  cplem1  9804  carduniima  10009  alephfp  10021  kmlem2  10065  isf32lem3  10268  domtriomlem  10355  axdc3lem2  10364  zorn2lem7  10415  ttukeylem6  10427  iundom2g  10453  fpwwe2lem12  10556  tskss  10672  tskr1om2  10682  inatsk  10692  gruss  10710  gruel  10717  grur1  10734  prlem934  10947  ltexprlem7  10956  supsr  11026  dedekind  11300  supadd  12115  supmullem2  12118  uzind  12612  iccsplit  13429  elfz0add  13571  predfz  13598  elfzoextl  13667  fsuppmapnn0fiub  13944  ccatval2  14531  swrdswrd  14658  pfxccatin12lem2a  14680  swrdccatin2  14682  pfxccatpfx2  14690  cshimadifsn0  14783  01sqrexlem6  15200  isercolllem2  15619  fsumcvg  15665  isumrpcl  15799  fprodcvg  15886  rpnnen2lem4  16175  fproddvdsd  16295  saddisj  16425  sadass  16431  bitsshft  16435  smuval2  16442  smupvallem  16443  smu01lem  16445  smueqlem  16450  reumodprminv  16766  ramub1lem1  16988  firest  17386  mrissmrid  17598  initoeu2lem0  17971  acsfiindd  18510  acsmapd  18511  dirge  18560  chndss  18573  issubmnd  18720  issubg2  19108  eqgid  19146  cyccom  19169  dprdff  19980  dprddisj2  20007  ablfac1c  20039  c0rnghm  20503  issubrng2  20526  subrgdvds  20554  issubrg2  20560  rnghmsscmap  20598  rngcsect  20604  funcrngcsetc  20608  rhmsscmap  20627  rhmsscrnghm  20633  ringcsect  20638  funcringcsetc  20642  rhmsubclem4  20656  lssssr  20940  lssats2  20986  lbspss  21069  lsmelval2  21072  lspprat  21143  lbsextlem2  21149  lbsextlem3  21150  rnglidlmmgm  21235  rnglidlmsgrp  21236  rnglidlrng  21237  lpigen  21325  psgndiflemB  21590  lsmcss  21682  obselocv  21718  f1lindf  21812  issubassa3  21856  mplcoe5lem  22027  mdetdiaglem  22573  cpmadugsumlemF  22851  toprntopon  22900  elcls  23048  clsndisj  23050  elcls3  23058  neindisj  23092  lpval  23114  lpsscls  23116  lpss3  23119  maxlp  23122  restntr  23157  ordtbas2  23166  ordtbas  23167  pnfnei  23195  mnfnei  23196  cncls2  23248  lmcnp  23279  lpcls  23339  hauscmplem  23381  2ndcdisj  23431  kgen2ss  23530  txuni2  23540  ptpjpre1  23546  tx1cn  23584  tx2cn  23585  prdstopn  23603  txlm  23623  imasnopn  23665  imasncld  23666  imasncls  23667  tgqtop  23687  regr1lem  23714  fgss2  23849  uzfbas  23873  ufilmax  23882  uffix2  23899  ufildr  23906  fmfnfmlem1  23929  fmco  23936  flimrest  23958  fclsopn  23989  fclscf  24000  flimfcls  24001  alexsubALTlem4  24025  qustgplem  24096  imasf1oxms  24464  prdsbl  24466  metrest  24499  iccntr  24797  reconnlem2  24803  caucfil  25260  caussi  25274  bcthlem5  25305  ovoliunlem1  25479  shft2rab  25485  sca2rab  25489  ovolicc2  25499  vitalilem2  25586  vitalilem5  25589  mbfinf  25642  i1f1lem  25666  mbfi1fseqlem4  25695  itgss  25789  itgcn  25822  c1liplem1  25973  c1lip1  25974  c1lip3  25976  ply1remlem  26140  plyexmo  26290  taylply2  26344  lgamucov  27015  fsumvma  27190  logfaclbnd  27199  ltsres  27640  nosepssdm  27664  nodenselem8  27669  nosupno  27681  nosupbday  27683  noinfbday  27698  elmade  27863  oldssmade  27873  mulsproplem13  28134  mulsproplem14  28135  precsexlem10  28222  bdayons  28282  uzsind  28411  axlowdimlem16  29040  axcontlem9  29055  edgupgr  29217  upgredg  29220  subgreldmiedg  29366  upgrres1  29396  crctcshwlkn0lem2  29894  wwlksnred  29975  clwwlkccatlem  30074  clwwlkf  30132  wwlksubclwwlk  30143  eupth2lems  30323  sspmval  30819  sspimsval  30824  ubthlem1  30956  shsubcl  31306  shorth  31381  elspansn3  31658  elnlfn  32014  elpjrn  32276  sumdmdlem2  32505  nfpconfp  32720  xrofsup  32855  elrspunidl  33503  ressply1mon1p  33643  fldextrspunlsplem  33833  cmpcref  34010  zarclsiin  34031  cntmeas  34386  1stmbfm  34420  2ndmbfm  34421  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemodife  34658  ballotlemimin  34666  bnj1171  35158  bnj1280  35178  r1filimi  35262  subgrwlk  35330  gonarlem  35592  goalrlem  35594  mrsubrn  35711  elfzm12  35873  ontgval  36629  elttctr  36703  bj-restuni  37425  pibt2  37747  lindsenlbs  37950  poimirlem29  37984  poimirlem30  37985  poimirlem31  37986  itg2addnclem  38006  itg2addnclem2  38007  ftc1anclem7  38034  ismtyima  38138  suceldisj  39153  lshpkr  39577  psubatN  40215  elpaddn0  40260  pclfinN  40360  diael  41503  dia2dimlem12  41535  dicelval1stN  41648  dicelval2nd  41649  dib2dim  41703  dih2dimbALTN  41705  dihlspsnssN  41792  dvh1dim  41902  lcfrvalsnN  42001  mapdrvallem2  42105  mapdpglem2  42133  hdmap10lem  42299  hdmap11lem2  42302  hdmapoc  42391  primrootscoprbij  42555  primrootspoweq0  42559  aks6d1c2  42583  sticksstones3  42601  sticksstones17  42616  sticksstones18  42617  unitscyglem2  42649  unitscyglem4  42651  unitscyglem5  42652  isnacs3  43156  aomclem2  43501  kelac1  43509  rngunsnply  43615  safesnsupfiub  43861  intabssd  43964  iunrelexp0  44147  rfovcnvf1od  44449  rfovcnvfvd  44452  fsovrfovd  44454  clsk1indlem3  44488  neik0pk1imk0  44492  ntrneineine0lem  44528  ntrneiel2  44531  ntrneikb  44539  ntrneik4w  44545  mnuop3d  44716  dvconstbi  44779  expgrowth  44780  modelaxreplem2  45424  modelaxreplem3  45425  climsuselem1  46055  climsuse  46056  limcresiooub  46088  iblsplit  46412  iblspltprt  46419  stoweidlem62  46508  stirlinglem11  46530  fourierdlem41  46594  qndenserrnbllem  46740  sge0fodjrnlem  46862  smflimsuplem7  47272  fafvelcdm  47630  fafv2elcdm  47694  ceilhalfelfzo1  47794  smonoord  47837  muldvdsfacm1  47847  iccpartiltu  47894  iccpartigtl  47895  iccpartiun  47906  iccpartdisj  47909  bgoldbtbndlem2  48294  gpgedgvtx1  48550  lidldomn1  48719  rhmsubcALTVlem4  48772  funcringcsetcALTV2lem9  48786  lincresunit3lem1  48967  setrec1  50178  setis  50185  vsetrec  50190  pgindnf  50203