Theorem sseld 3942

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-clel 2803  df-ss 3928

This theorem is referenced by:  sselda  3943  sseldd  3944  ssneld  3945  eqrrabd  4045  elelpwi  4569  ssbrd  5145  uniopel  5471  exopxfr2  5798  dmrnssfld  5926  preddowncl  6293  opelf  6703  elfvunirn  6872  fimarab  6917  fvimacnv  7007  ffvelcdm  7035  fnsnr  7119  f1imass  7221  onminex  7758  xpord2pred  8101  extmptsuppeq  8144  suppssr  8151  suppssrg  8152  dftpos3  8200  oa00  8500  omordi  8507  omlimcl  8519  omeulem1  8523  nnmordi  8572  mapsnd  8836  ixpf  8870  pw2f1olem  9022  pssnn  9109  findcard3  9205  findcard3OLD  9206  ixpfi2  9277  fissuni  9284  elfiun  9357  dffi3  9358  supssd  9390  infssd  9421  ordiso2  9444  ordtypelem7  9453  ixpiunwdom  9519  inf3lem2  9558  cantnfp1lem3  9609  cantnfp1  9610  cantnflem1  9618  cantnf  9622  trcl  9657  r1ordg  9707  rankelb  9753  rankuni2b  9782  rankval4  9796  tcrank  9813  cplem1  9818  carduniima  10025  alephfp  10037  kmlem2  10081  isf32lem3  10284  domtriomlem  10371  axdc3lem2  10380  zorn2lem7  10431  ttukeylem6  10443  iundom2g  10469  fpwwe2lem12  10571  tskss  10687  tskr1om2  10697  inatsk  10707  gruss  10725  gruel  10732  grur1  10749  prlem934  10962  ltexprlem7  10971  supsr  11041  dedekind  11313  supadd  12127  supmullem2  12130  uzind  12602  iccsplit  13422  elfz0add  13563  predfz  13590  elfzoextl  13658  fsuppmapnn0fiub  13932  ccatval2  14519  swrdswrd  14646  pfxccatin12lem2a  14668  swrdccatin2  14670  pfxccatpfx2  14678  cshimadifsn0  14772  01sqrexlem6  15189  isercolllem2  15608  fsumcvg  15654  isumrpcl  15785  fprodcvg  15872  rpnnen2lem4  16161  fproddvdsd  16281  saddisj  16411  sadass  16417  bitsshft  16421  smuval2  16428  smupvallem  16429  smu01lem  16431  smueqlem  16436  reumodprminv  16751  ramub1lem1  16973  firest  17371  mrissmrid  17578  initoeu2lem0  17951  acsfiindd  18488  acsmapd  18489  dirge  18538  issubmnd  18664  issubg2  19049  eqgid  19088  cyccom  19111  dprdff  19920  dprddisj2  19947  ablfac1c  19979  c0rnghm  20420  issubrng2  20443  subrgdvds  20471  issubrg2  20477  rnghmsscmap  20515  rngcsect  20521  funcrngcsetc  20525  rhmsscmap  20544  rhmsscrnghm  20550  ringcsect  20555  funcringcsetc  20559  rhmsubclem4  20573  lssssr  20836  lssats2  20882  lbspss  20965  lsmelval2  20968  lspprat  21039  lbsextlem2  21045  lbsextlem3  21046  rnglidlmmgm  21131  rnglidlmsgrp  21132  rnglidlrng  21133  lpigen  21221  psgndiflemB  21485  lsmcss  21577  obselocv  21613  f1lindf  21707  issubassa3  21751  mplcoe5lem  21922  mdetdiaglem  22461  cpmadugsumlemF  22739  toprntopon  22788  elcls  22936  clsndisj  22938  elcls3  22946  neindisj  22980  lpval  23002  lpsscls  23004  lpss3  23007  maxlp  23010  restntr  23045  ordtbas2  23054  ordtbas  23055  pnfnei  23083  mnfnei  23084  cncls2  23136  lmcnp  23167  lpcls  23227  hauscmplem  23269  2ndcdisj  23319  kgen2ss  23418  txuni2  23428  ptpjpre1  23434  tx1cn  23472  tx2cn  23473  prdstopn  23491  txlm  23511  imasnopn  23553  imasncld  23554  imasncls  23555  tgqtop  23575  regr1lem  23602  fgss2  23737  uzfbas  23761  ufilmax  23770  uffix2  23787  ufildr  23794  fmfnfmlem1  23817  fmco  23824  flimrest  23846  fclsopn  23877  fclscf  23888  flimfcls  23889  alexsubALTlem4  23913  qustgplem  23984  imasf1oxms  24353  prdsbl  24355  metrest  24388  iccntr  24686  reconnlem2  24692  caucfil  25159  caussi  25173  bcthlem5  25204  ovoliunlem1  25379  shft2rab  25385  sca2rab  25389  ovolicc2  25399  vitalilem2  25486  vitalilem5  25489  mbfinf  25542  i1f1lem  25566  mbfi1fseqlem4  25595  itgss  25689  itgcn  25722  c1liplem1  25877  c1lip1  25878  c1lip3  25880  ply1remlem  26046  plyexmo  26197  taylply2  26251  lgamucov  26924  fsumvma  27100  logfaclbnd  27109  sltres  27550  nosepssdm  27574  nodenselem8  27579  nosupno  27591  nosupbday  27593  noinfbday  27608  elmade  27755  oldssmade  27765  mulsproplem13  28007  mulsproplem14  28008  precsexlem10  28094  bdayon  28149  uzsind  28269  axlowdimlem16  28860  axcontlem9  28875  edgupgr  29037  upgredg  29040  subgreldmiedg  29186  upgrres1  29216  crctcshwlkn0lem2  29714  wwlksnred  29795  clwwlkccatlem  29891  clwwlkf  29949  wwlksubclwwlk  29960  eupth2lems  30140  sspmval  30635  sspimsval  30640  ubthlem1  30772  shsubcl  31122  shorth  31197  elspansn3  31474  elnlfn  31830  elpjrn  32092  sumdmdlem2  32321  nfpconfp  32529  xrofsup  32663  elrspunidl  33372  ressply1mon1p  33510  fldextrspunlsplem  33641  cmpcref  33813  zarclsiin  33834  cntmeas  34189  1stmbfm  34224  2ndmbfm  34225  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  ballotlemimin  34470  bnj1171  34963  bnj1280  34983  subgrwlk  35092  gonarlem  35354  goalrlem  35356  mrsubrn  35473  elfzm12  35635  ontgval  36392  bj-restuni  37058  pibt2  37378  lindsenlbs  37582  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  itg2addnclem  37638  itg2addnclem2  37639  ftc1anclem7  37666  ismtyima  37770  lshpkr  39083  psubatN  39722  elpaddn0  39767  pclfinN  39867  diael  41010  dia2dimlem12  41042  dicelval1stN  41155  dicelval2nd  41156  dib2dim  41210  dih2dimbALTN  41212  dihlspsnssN  41299  dvh1dim  41409  lcfrvalsnN  41508  mapdrvallem2  41612  mapdpglem2  41640  hdmap10lem  41806  hdmap11lem2  41809  hdmapoc  41898  primrootscoprbij  42063  primrootspoweq0  42067  aks6d1c2  42091  sticksstones3  42109  sticksstones17  42124  sticksstones18  42125  unitscyglem2  42157  unitscyglem4  42159  unitscyglem5  42160  isnacs3  42671  aomclem2  43017  kelac1  43025  rngunsnply  43131  safesnsupfiub  43378  intabssd  43481  iunrelexp0  43664  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovrfovd  43971  clsk1indlem3  44005  neik0pk1imk0  44009  ntrneineine0lem  44045  ntrneiel2  44048  ntrneikb  44056  ntrneik4w  44062  mnuop3d  44233  dvconstbi  44296  expgrowth  44297  modelaxreplem2  44942  modelaxreplem3  44943  climsuselem1  45578  climsuse  45579  limcresiooub  45613  iblsplit  45937  iblspltprt  45944  stoweidlem62  46033  stirlinglem11  46055  fourierdlem41  46119  qndenserrnbllem  46265  sge0fodjrnlem  46387  smflimsuplem7  46797  fafvelcdm  47144  fafv2elcdm  47208  ceilhalfelfzo1  47304  smonoord  47345  iccpartiltu  47396  iccpartigtl  47397  iccpartiun  47408  iccpartdisj  47411  bgoldbtbndlem2  47780  gpgedgvtx1  48026  lidldomn1  48192  rhmsubcALTVlem4  48245  funcringcsetcALTV2lem9  48259  lincresunit3lem1  48441  setrec1  49653  setis  49660  vsetrec  49665  pgindnf  49678