Theorem sseld 3914

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 3909	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2119   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-clel 2814  df-ss 3900

This theorem is referenced by:  sselda  3915  sseldd  3916  ssneld  3917  eqrrabd  4017  elelpwi  4539  ssbrd  5115  uniopel  5457  exopxfr2  5786  dmrnssfld  5916  preddowncl  6283  opelf  6688  elfvunirn  6857  fimarab  6901  fvimacnv  6994  ffvelcdm  7022  fnsnr  7107  f1imass  7208  onminex  7745  xpord2pred  8085  extmptsuppeq  8128  suppssr  8135  suppssrg  8136  dftpos3  8184  oa00  8484  omordi  8491  omlimcl  8503  omeulem1  8507  nnmordi  8557  mapsnd  8824  ixpf  8858  pw2f1olem  9009  pssnn  9093  findcard3  9183  ixpfi2  9250  fissuni  9257  elfiun  9333  dffi3  9334  supssd  9366  infssd  9397  ordiso2  9420  ordtypelem7  9429  ixpiunwdom  9495  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  20507  issubrng2  20530  subrgdvds  20558  issubrg2  20564  rnghmsscmap  20602  rngcsect  20608  funcrngcsetc  20612  rhmsscmap  20631  rhmsscrnghm  20637  ringcsect  20642  funcringcsetc  20646  rhmsubclem4  20660  lssssr  20944  lssats2  20990  lbspss  21072  lsmelval2  21075  lspprat  21146  lbsextlem2  21152  lbsextlem3  21153  rnglidlmmgm  21238  rnglidlmsgrp  21239  rnglidlrng  21240  lpigen  21328  psgndiflemB  21575  lsmcss  21667  obselocv  21703  f1lindf  21797  issubassa3  21841  mplcoe5lem  22015  mdetdiaglem  22581  cpmadugsumlemF  22859  toprntopon  22908  elcls  23056  clsndisj  23058  elcls3  23066  neindisj  23100  lpval  23122  lpsscls  23124  lpss3  23127  maxlp  23130  restntr  23165  ordtbas2  23174  ordtbas  23175  pnfnei  23203  mnfnei  23204  cncls2  23256  lmcnp  23287  lpcls  23347  hauscmplem  23389  2ndcdisj  23439  kgen2ss  23538  txuni2  23548  ptpjpre1  23554  tx1cn  23592  tx2cn  23593  prdstopn  23611  txlm  23631  imasnopn  23673  imasncld  23674  imasncls  23675  tgqtop  23695  regr1lem  23722  fgss2  23857  uzfbas  23881  ufilmax  23890  uffix2  23907  ufildr  23914  fmfnfmlem1  23937  fmco  23944  flimrest  23966  fclsopn  23997  fclscf  24008  flimfcls  24009  alexsubALTlem4  24033  qustgplem  24104  imasf1oxms  24472  prdsbl  24474  metrest  24507  iccntr  24805  reconnlem2  24811  caucfil  25268  caussi  25282  bcthlem5  25313  ovoliunlem1  25487  shft2rab  25493  sca2rab  25497  ovolicc2  25507  vitalilem2  25594  vitalilem5  25597  mbfinf  25650  i1f1lem  25674  mbfi1fseqlem4  25703  itgss  25797  itgcn  25830  c1liplem1  25981  c1lip1  25982  c1lip3  25984  ply1remlem  26148  plyexmo  26297  taylply2  26351  lgamucov  27019  fsumvma  27194  logfaclbnd  27203  ltsres  27644  nosepssdm  27668  nodenselem8  27673  nosupno  27685  nosupbday  27687  noinfbday  27702  elmade  27867  oldssmade  27877  mulsproplem13  28138  mulsproplem14  28139  precsexlem10  28226  bdayons  28286  uzsind  28415  axlowdimlem16  29044  axcontlem9  29059  edgupgr  29221  upgredg  29224  subgreldmiedg  29370  upgrres1  29400  crctcshwlkn0lem2  29897  wwlksnred  29978  clwwlkccatlem  30077  clwwlkf  30135  wwlksubclwwlk  30146  eupth2lems  30326  sspmval  30822  sspimsval  30827  ubthlem1  30959  shsubcl  31309  shorth  31384  elspansn3  31661  elnlfn  32017  elpjrn  32279  sumdmdlem2  32508  nfpconfp  32724  xrofsup  32859  elrspunidl  33511  ressply1mon1p  33651  fldextrspunlsplem  33857  cmpcref  34034  zarclsiin  34055  cntmeas  34410  1stmbfm  34444  2ndmbfm  34445  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemodife  34682  ballotlemimin  34690  bnj1171  35182  bnj1280  35202  r1filimi  35284  subgrwlk  35360  gonarlem  35622  goalrlem  35624  mrsubrn  35741  elfzm12  35903  ontgval  36659  elttctr  36733  bj-restuni  37455  pibt2  37779  lindsenlbs  37982  poimirlem29  38016  poimirlem30  38017  poimirlem31  38018  itg2addnclem  38038  itg2addnclem2  38039  ftc1anclem7  38066  ismtyima  38170  suceldisj  39185  lshpkr  39609  psubatN  40247  elpaddn0  40292  pclfinN  40392  diael  41535  dia2dimlem12  41567  dicelval1stN  41680  dicelval2nd  41681  dib2dim  41735  dih2dimbALTN  41737  dihlspsnssN  41824  dvh1dim  41934  lcfrvalsnN  42033  mapdrvallem2  42137  mapdpglem2  42165  hdmap10lem  42331  hdmap11lem2  42334  hdmapoc  42423  primrootscoprbij  42587  primrootspoweq0  42591  aks6d1c2  42615  sticksstones3  42633  sticksstones17  42648  sticksstones18  42649  unitscyglem2  42681  unitscyglem4  42683  unitscyglem5  42684  isnacs3  43159  aomclem2  43500  kelac1  43508  rngunsnply  43614  safesnsupfiub  43860  intabssd  43963  iunrelexp0  44146  rfovcnvf1od  44448  rfovcnvfvd  44451  fsovrfovd  44453  clsk1indlem3  44487  neik0pk1imk0  44491  ntrneineine0lem  44527  ntrneiel2  44530  ntrneikb  44538  ntrneik4w  44544  mnuop3d  44715  dvconstbi  44778  expgrowth  44779  modelaxreplem2  45423  modelaxreplem3  45424  climsuselem1  46052  climsuse  46053  limcresiooub  46085  iblsplit  46409  iblspltprt  46416  stoweidlem62  46505  stirlinglem11  46527  fourierdlem41  46591  qndenserrnbllem  46737  sge0fodjrnlem  46859  smflimsuplem7  47269  fafvelcdm  47633  fafv2elcdm  47697  ceilhalfelfzo1  47797  smonoord  47840  muldvdsfacm1  47850  iccpartiltu  47897  iccpartigtl  47898  iccpartiun  47909  iccpartdisj  47912  bgoldbtbndlem2  48297  gpgedgvtx1  48553  lidldomn1  48722  rhmsubcALTVlem4  48775  funcringcsetcALTV2lem9  48789  lincresunit3lem1  48970  setrec1  50181  setis  50188  vsetrec  50193  pgindnf  50206