Theorem sseld 3886

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

Syntax hints:   → wi 4   ∈ wcel 2112   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  sselda  3887  sseldd  3888  ssneld  3889  elelpwi  4511  ssbrd  5082  uniopel  5384  exopxfr2  5698  dmrnssfld  5824  preddowncl  6168  opelf  6558  fvimacnv  6851  ffvelrn  6880  fnsnr  6958  f1imass  7054  onminex  7564  extmptsuppeq  7908  suppssr  7916  suppssrg  7917  dftpos3  7964  wfrlem16  8048  oa00  8265  omordi  8272  omlimcl  8284  omeulem1  8288  nnmordi  8337  mapsnd  8545  ixpf  8579  pw2f1olem  8727  pssnn  8824  pssnnOLD  8872  findcard3  8892  ixpfi2  8952  fissuni  8959  elfiun  9024  dffi3  9025  ordiso2  9109  ordtypelem7  9118  ixpiunwdom  9184  inf3lem2  9222  cantnfp1lem3  9273  cantnfp1  9274  cantnflem1  9282  cantnf  9286  trpredtr  9313  trpredmintr  9314  dftrpred3g  9317  trpredrec  9320  trcl  9322  r1ordg  9359  rankelb  9405  rankuni2b  9434  rankval4  9448  tcrank  9465  cplem1  9470  carduniima  9675  alephfp  9687  kmlem2  9730  isf32lem3  9934  domtriomlem  10021  axdc3lem2  10030  zorn2lem7  10081  ttukeylem6  10093  iundom2g  10119  fpwwe2lem12  10221  tskss  10337  tskr1om2  10347  inatsk  10357  gruss  10375  gruel  10382  grur1  10399  prlem934  10612  ltexprlem7  10621  supsr  10691  dedekind  10960  supadd  11765  supmullem2  11768  uzind  12234  iccsplit  13038  elfz0add  13176  predfz  13202  fsuppmapnn0fiub  13529  ccatval2  14100  swrdswrd  14235  pfxccatin12lem2a  14257  swrdccatin2  14259  pfxccatpfx2  14267  cshimadifsn0  14360  sqrlem6  14776  isercolllem2  15194  fsumcvg  15241  isumrpcl  15370  fprodcvg  15455  rpnnen2lem4  15741  fproddvdsd  15859  saddisj  15987  sadass  15993  bitsshft  15997  smuval2  16004  smupvallem  16005  smu01lem  16007  smueqlem  16012  reumodprminv  16320  ramub1lem1  16542  firest  16891  mrissmrid  17098  initoeu2lem0  17473  acsfiindd  18013  acsmapd  18014  dirge  18063  issubmnd  18154  issubg2  18512  eqgid  18550  cyccom  18564  dprdff  19353  dprddisj2  19380  ablfac1c  19412  subrgdvds  19768  issubrg2  19774  lssssr  19944  lssats2  19991  lbspss  20073  lsmelval2  20076  lspprat  20144  lbsextlem2  20150  lbsextlem3  20151  lpigen  20248  psgndiflemB  20516  lsmcss  20608  obselocv  20644  f1lindf  20738  issubassa3  20781  mplcoe5lem  20950  mdetdiaglem  21449  cpmadugsumlemF  21727  toprntopon  21776  elcls  21924  clsndisj  21926  elcls3  21934  neindisj  21968  lpval  21990  lpsscls  21992  lpss3  21995  maxlp  21998  restntr  22033  ordtbas2  22042  ordtbas  22043  pnfnei  22071  mnfnei  22072  cncls2  22124  lmcnp  22155  lpcls  22215  hauscmplem  22257  2ndcdisj  22307  kgen2ss  22406  txuni2  22416  ptpjpre1  22422  tx1cn  22460  tx2cn  22461  prdstopn  22479  txlm  22499  imasnopn  22541  imasncld  22542  imasncls  22543  tgqtop  22563  regr1lem  22590  fgss2  22725  uzfbas  22749  ufilmax  22758  uffix2  22775  ufildr  22782  fmfnfmlem1  22805  fmco  22812  flimrest  22834  fclsopn  22865  fclscf  22876  flimfcls  22877  alexsubALTlem4  22901  qustgplem  22972  imasf1oxms  23341  prdsbl  23343  metrest  23376  iccntr  23672  reconnlem2  23678  caucfil  24134  caussi  24148  bcthlem5  24179  ovoliunlem1  24353  shft2rab  24359  sca2rab  24363  ovolicc2  24373  vitalilem2  24460  vitalilem5  24463  mbfinf  24516  i1f1lem  24540  mbfi1fseqlem4  24570  itgss  24663  itgcn  24696  c1liplem1  24847  c1lip1  24848  c1lip3  24850  ply1remlem  25014  plyexmo  25160  lgamucov  25874  fsumvma  26048  logfaclbnd  26057  axlowdimlem16  27002  axcontlem9  27017  edgupgr  27179  upgredg  27182  subgreldmiedg  27325  upgrres1  27355  crctcshwlkn0lem2  27849  wwlksnred  27930  clwwlkccatlem  28026  clwwlkf  28084  wwlksubclwwlk  28095  eupth2lems  28275  sspmval  28768  sspimsval  28773  ubthlem1  28905  shsubcl  29255  shorth  29330  elspansn3  29607  elnlfn  29963  elpjrn  30225  sumdmdlem2  30454  eqrrabd  30522  nfpconfp  30640  fimarab  30653  supssd  30718  infssd  30719  xrofsup  30764  elrspunidl  31274  cmpcref  31468  zarclsiin  31489  cntmeas  31860  1stmbfm  31893  2ndmbfm  31894  ballotlemfc0  32125  ballotlemfcc  32126  ballotlemodife  32130  ballotlemimin  32138  bnj1171  32647  bnj1280  32667  subgrwlk  32761  gonarlem  33023  goalrlem  33025  mrsubrn  33142  elfzm12  33300  xpord2pred  33472  sltres  33551  nosepssdm  33575  nodenselem8  33580  nosupno  33592  nosupbday  33594  noinfbday  33609  elmade  33737  oldssmade  33746  ontgval  34306  bj-restuni  34952  pibt2  35274  lindsenlbs  35458  poimirlem29  35492  poimirlem30  35493  poimirlem31  35494  itg2addnclem  35514  itg2addnclem2  35515  ftc1anclem7  35542  ismtyima  35647  lshpkr  36817  psubatN  37455  elpaddn0  37500  pclfinN  37600  diael  38743  dia2dimlem12  38775  dicelval1stN  38888  dicelval2nd  38889  dib2dim  38943  dih2dimbALTN  38945  dihlspsnssN  39032  dvh1dim  39142  lcfrvalsnN  39241  mapdrvallem2  39345  mapdpglem2  39373  hdmap10lem  39539  hdmap11lem2  39542  hdmapoc  39631  sticksstones3  39773  isnacs3  40176  aomclem2  40524  kelac1  40532  rngunsnply  40642  intabssd  40752  iunrelexp0  40928  rfovcnvf1od  41230  rfovcnvfvd  41233  fsovrfovd  41235  clsk1indlem3  41271  neik0pk1imk0  41275  ntrneineine0lem  41311  ntrneiel2  41314  ntrneikb  41322  ntrneik4w  41328  mnuop3d  41503  dvconstbi  41566  expgrowth  41567  climsuselem1  42766  climsuse  42767  limcresiooub  42801  iblsplit  43125  iblspltprt  43132  stoweidlem62  43221  stirlinglem11  43243  fourierdlem41  43307  qndenserrnbllem  43453  sge0fodjrnlem  43572  sssmf  43889  smflimsuplem7  43974  fafvelrn  44277  fafv2elrn  44341  smonoord  44439  iccpartiltu  44490  iccpartigtl  44491  iccpartiun  44502  iccpartdisj  44505  bgoldbtbndlem2  44874  c0rnghm  45087  lidldomn1  45095  lidlmmgm  45099  lidlmsgrp  45100  lidlrng  45101  rnghmsscmap  45148  rngcsect  45154  funcrngcsetc  45172  rhmsscmap  45194  rhmsscrnghm  45200  ringcsect  45205  funcringcsetc  45209  funcringcsetcALTV2lem9  45218  rhmsubclem4  45263  rhmsubcALTVlem4  45281  lincresunit3lem1  45436  setrec1  46011  setis  46017  vsetrec  46022