Theorem sseld 3964

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2808  df-ss 3950

This theorem is referenced by:  sselda  3965  sseldd  3966  ssneld  3967  eqrrabd  4068  elelpwi  4592  ssbrd  5168  uniopel  5503  exopxfr2  5837  dmrnssfld  5966  preddowncl  6334  opelf  6750  elfvunirn  6919  fimarab  6964  fvimacnv  7054  ffvelcdm  7082  fnsnr  7166  f1imass  7267  onminex  7805  xpord2pred  8153  extmptsuppeq  8196  suppssr  8203  suppssrg  8204  dftpos3  8252  wfrlem16OLD  8347  oa00  8580  omordi  8587  omlimcl  8599  omeulem1  8603  nnmordi  8652  mapsnd  8909  ixpf  8943  pw2f1olem  9099  pssnn  9191  findcard3  9301  findcard3OLD  9302  ixpfi2  9373  fissuni  9380  elfiun  9453  dffi3  9454  ordiso2  9538  ordtypelem7  9547  ixpiunwdom  9613  inf3lem2  9652  cantnfp1lem3  9703  cantnfp1  9704  cantnflem1  9712  cantnf  9716  trcl  9751  r1ordg  9801  rankelb  9847  rankuni2b  9876  rankval4  9890  tcrank  9907  cplem1  9912  carduniima  10119  alephfp  10131  kmlem2  10175  isf32lem3  10378  domtriomlem  10465  axdc3lem2  10474  zorn2lem7  10525  ttukeylem6  10537  iundom2g  10563  fpwwe2lem12  10665  tskss  10781  tskr1om2  10791  inatsk  10801  gruss  10819  gruel  10826  grur1  10843  prlem934  11056  ltexprlem7  11065  supsr  11135  dedekind  11407  supadd  12219  supmullem2  12222  uzind  12694  iccsplit  13508  elfz0add  13649  predfz  13676  elfzoextl  13743  fsuppmapnn0fiub  14015  ccatval2  14599  swrdswrd  14726  pfxccatin12lem2a  14748  swrdccatin2  14750  pfxccatpfx2  14758  cshimadifsn0  14852  01sqrexlem6  15269  isercolllem2  15685  fsumcvg  15731  isumrpcl  15862  fprodcvg  15949  rpnnen2lem4  16236  fproddvdsd  16355  saddisj  16485  sadass  16491  bitsshft  16495  smuval2  16502  smupvallem  16503  smu01lem  16505  smueqlem  16510  reumodprminv  16825  ramub1lem1  17047  firest  17453  mrissmrid  17660  initoeu2lem0  18034  acsfiindd  18572  acsmapd  18573  dirge  18622  issubmnd  18748  issubg2  19133  eqgid  19172  cyccom  19195  dprdff  20005  dprddisj2  20032  ablfac1c  20064  c0rnghm  20508  issubrng2  20531  subrgdvds  20559  issubrg2  20565  rnghmsscmap  20603  rngcsect  20609  funcrngcsetc  20613  rhmsscmap  20632  rhmsscrnghm  20638  ringcsect  20643  funcringcsetc  20647  rhmsubclem4  20661  lssssr  20925  lssats2  20971  lbspss  21054  lsmelval2  21057  lspprat  21128  lbsextlem2  21134  lbsextlem3  21135  rnglidlmmgm  21222  rnglidlmsgrp  21223  rnglidlrng  21224  lpigen  21312  psgndiflemB  21585  lsmcss  21677  obselocv  21715  f1lindf  21809  issubassa3  21853  mplcoe5lem  22024  mdetdiaglem  22571  cpmadugsumlemF  22849  toprntopon  22898  elcls  23046  clsndisj  23048  elcls3  23056  neindisj  23090  lpval  23112  lpsscls  23114  lpss3  23117  maxlp  23120  restntr  23155  ordtbas2  23164  ordtbas  23165  pnfnei  23193  mnfnei  23194  cncls2  23246  lmcnp  23277  lpcls  23337  hauscmplem  23379  2ndcdisj  23429  kgen2ss  23528  txuni2  23538  ptpjpre1  23544  tx1cn  23582  tx2cn  23583  prdstopn  23601  txlm  23621  imasnopn  23663  imasncld  23664  imasncls  23665  tgqtop  23685  regr1lem  23712  fgss2  23847  uzfbas  23871  ufilmax  23880  uffix2  23897  ufildr  23904  fmfnfmlem1  23927  fmco  23934  flimrest  23956  fclsopn  23987  fclscf  23998  flimfcls  23999  alexsubALTlem4  24023  qustgplem  24094  imasf1oxms  24465  prdsbl  24467  metrest  24500  iccntr  24798  reconnlem2  24804  caucfil  25272  caussi  25286  bcthlem5  25317  ovoliunlem1  25492  shft2rab  25498  sca2rab  25502  ovolicc2  25512  vitalilem2  25599  vitalilem5  25602  mbfinf  25655  i1f1lem  25679  mbfi1fseqlem4  25708  itgss  25802  itgcn  25835  c1liplem1  25990  c1lip1  25991  c1lip3  25993  ply1remlem  26159  plyexmo  26310  taylply2  26364  lgamucov  27036  fsumvma  27212  logfaclbnd  27221  sltres  27662  nosepssdm  27686  nodenselem8  27691  nosupno  27703  nosupbday  27705  noinfbday  27720  elmade  27861  oldssmade  27871  mulsproplem13  28109  mulsproplem14  28110  precsexlem10  28195  uzsind  28346  axlowdimlem16  28921  axcontlem9  28936  edgupgr  29098  upgredg  29101  subgreldmiedg  29247  upgrres1  29277  crctcshwlkn0lem2  29778  wwlksnred  29859  clwwlkccatlem  29955  clwwlkf  30013  wwlksubclwwlk  30024  eupth2lems  30204  sspmval  30699  sspimsval  30704  ubthlem1  30836  shsubcl  31186  shorth  31261  elspansn3  31538  elnlfn  31894  elpjrn  32156  sumdmdlem2  32385  nfpconfp  32589  supssd  32668  infssd  32669  xrofsup  32718  elrspunidl  33397  ressply1mon1p  33534  fldextrspunlsplem  33664  cmpcref  33790  zarclsiin  33811  cntmeas  34168  1stmbfm  34203  2ndmbfm  34204  ballotlemfc0  34436  ballotlemfcc  34437  ballotlemodife  34441  ballotlemimin  34449  bnj1171  34955  bnj1280  34975  subgrwlk  35078  gonarlem  35340  goalrlem  35342  mrsubrn  35459  elfzm12  35621  ontgval  36373  bj-restuni  37039  pibt2  37359  lindsenlbs  37563  poimirlem29  37597  poimirlem30  37598  poimirlem31  37599  itg2addnclem  37619  itg2addnclem2  37620  ftc1anclem7  37647  ismtyima  37751  lshpkr  39059  psubatN  39698  elpaddn0  39743  pclfinN  39843  diael  40986  dia2dimlem12  41018  dicelval1stN  41131  dicelval2nd  41132  dib2dim  41186  dih2dimbALTN  41188  dihlspsnssN  41275  dvh1dim  41385  lcfrvalsnN  41484  mapdrvallem2  41588  mapdpglem2  41616  hdmap10lem  41782  hdmap11lem2  41785  hdmapoc  41874  primrootscoprbij  42044  primrootspoweq0  42048  aks6d1c2  42072  sticksstones3  42090  sticksstones17  42105  sticksstones18  42106  unitscyglem2  42138  unitscyglem4  42140  unitscyglem5  42141  isnacs3  42666  aomclem2  43012  kelac1  43020  rngunsnply  43126  safesnsupfiub  43374  intabssd  43477  iunrelexp0  43660  rfovcnvf1od  43962  rfovcnvfvd  43965  fsovrfovd  43967  clsk1indlem3  44001  neik0pk1imk0  44005  ntrneineine0lem  44041  ntrneiel2  44044  ntrneikb  44052  ntrneik4w  44058  mnuop3d  44235  dvconstbi  44298  expgrowth  44299  modelaxreplem2  44941  modelaxreplem3  44942  climsuselem1  45567  climsuse  45568  limcresiooub  45602  iblsplit  45926  iblspltprt  45933  stoweidlem62  46022  stirlinglem11  46044  fourierdlem41  46108  qndenserrnbllem  46254  sge0fodjrnlem  46376  smflimsuplem7  46786  fafvelcdm  47128  fafv2elcdm  47192  smonoord  47304  iccpartiltu  47355  iccpartigtl  47356  iccpartiun  47367  iccpartdisj  47370  bgoldbtbndlem2  47739  ceilhalfelfzo1  47962  gpgedgvtx1  47966  lidldomn1  48093  rhmsubcALTVlem4  48146  funcringcsetcALTV2lem9  48160  lincresunit3lem1  48342  setrec1  49206  setis  49213  vsetrec  49218  pgindnf  49231