Theorem sseld 3934

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

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

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 3920

This theorem is referenced by:  sselda  3935  sseldd  3936  ssneld  3937  eqrrabd  4040  elelpwi  4566  ssbrd  5143  uniopel  5472  exopxfr2  5801  dmrnssfld  5931  preddowncl  6298  opelf  6703  elfvunirn  6872  fimarab  6916  fvimacnv  7007  ffvelcdm  7035  fnsnr  7119  f1imass  7220  onminex  7757  xpord2pred  8097  extmptsuppeq  8140  suppssr  8147  suppssrg  8148  dftpos3  8196  oa00  8496  omordi  8503  omlimcl  8515  omeulem1  8519  nnmordi  8569  mapsnd  8836  ixpf  8870  pw2f1olem  9021  pssnn  9105  findcard3  9195  ixpfi2  9262  fissuni  9269  elfiun  9345  dffi3  9346  supssd  9378  infssd  9409  ordiso2  9432  ordtypelem7  9441  ixpiunwdom  9507  inf3lem2  9550  cantnfp1lem3  9601  cantnfp1  9602  cantnflem1  9610  cantnf  9614  trcl  9649  r1ordg  9702  rankelb  9748  rankuni2b  9777  rankval4  9791  tcrank  9808  cplem1  9813  carduniima  10018  alephfp  10030  kmlem2  10074  isf32lem3  10277  domtriomlem  10364  axdc3lem2  10373  zorn2lem7  10424  ttukeylem6  10436  iundom2g  10462  fpwwe2lem12  10565  tskss  10681  tskr1om2  10691  inatsk  10701  gruss  10719  gruel  10726  grur1  10743  prlem934  10956  ltexprlem7  10965  supsr  11035  dedekind  11308  supadd  12122  supmullem2  12125  uzind  12596  iccsplit  13413  elfz0add  13554  predfz  13581  elfzoextl  13649  fsuppmapnn0fiub  13926  ccatval2  14513  swrdswrd  14640  pfxccatin12lem2a  14662  swrdccatin2  14664  pfxccatpfx2  14672  cshimadifsn0  14765  01sqrexlem6  15182  isercolllem2  15601  fsumcvg  15647  isumrpcl  15778  fprodcvg  15865  rpnnen2lem4  16154  fproddvdsd  16274  saddisj  16404  sadass  16410  bitsshft  16414  smuval2  16421  smupvallem  16422  smu01lem  16424  smueqlem  16429  reumodprminv  16744  ramub1lem1  16966  firest  17364  mrissmrid  17576  initoeu2lem0  17949  acsfiindd  18488  acsmapd  18489  dirge  18538  chndss  18551  issubmnd  18698  issubg2  19083  eqgid  19121  cyccom  19144  dprdff  19955  dprddisj2  19982  ablfac1c  20014  c0rnghm  20480  issubrng2  20503  subrgdvds  20531  issubrg2  20537  rnghmsscmap  20575  rngcsect  20581  funcrngcsetc  20585  rhmsscmap  20604  rhmsscrnghm  20610  ringcsect  20615  funcringcsetc  20619  rhmsubclem4  20633  lssssr  20917  lssats2  20963  lbspss  21046  lsmelval2  21049  lspprat  21120  lbsextlem2  21126  lbsextlem3  21127  rnglidlmmgm  21212  rnglidlmsgrp  21213  rnglidlrng  21214  lpigen  21302  psgndiflemB  21567  lsmcss  21659  obselocv  21695  f1lindf  21789  issubassa3  21833  mplcoe5lem  22006  mdetdiaglem  22554  cpmadugsumlemF  22832  toprntopon  22881  elcls  23029  clsndisj  23031  elcls3  23039  neindisj  23073  lpval  23095  lpsscls  23097  lpss3  23100  maxlp  23103  restntr  23138  ordtbas2  23147  ordtbas  23148  pnfnei  23176  mnfnei  23177  cncls2  23229  lmcnp  23260  lpcls  23320  hauscmplem  23362  2ndcdisj  23412  kgen2ss  23511  txuni2  23521  ptpjpre1  23527  tx1cn  23565  tx2cn  23566  prdstopn  23584  txlm  23604  imasnopn  23646  imasncld  23647  imasncls  23648  tgqtop  23668  regr1lem  23695  fgss2  23830  uzfbas  23854  ufilmax  23863  uffix2  23880  ufildr  23887  fmfnfmlem1  23910  fmco  23917  flimrest  23939  fclsopn  23970  fclscf  23981  flimfcls  23982  alexsubALTlem4  24006  qustgplem  24077  imasf1oxms  24445  prdsbl  24447  metrest  24480  iccntr  24778  reconnlem2  24784  caucfil  25251  caussi  25265  bcthlem5  25296  ovoliunlem1  25471  shft2rab  25477  sca2rab  25481  ovolicc2  25491  vitalilem2  25578  vitalilem5  25581  mbfinf  25634  i1f1lem  25658  mbfi1fseqlem4  25687  itgss  25781  itgcn  25814  c1liplem1  25969  c1lip1  25970  c1lip3  25972  ply1remlem  26138  plyexmo  26289  taylply2  26343  lgamucov  27016  fsumvma  27192  logfaclbnd  27201  ltsres  27642  nosepssdm  27666  nodenselem8  27671  nosupno  27683  nosupbday  27685  noinfbday  27700  elmade  27865  oldssmade  27875  mulsproplem13  28136  mulsproplem14  28137  precsexlem10  28224  bdayons  28284  uzsind  28413  axlowdimlem16  29042  axcontlem9  29057  edgupgr  29219  upgredg  29222  subgreldmiedg  29368  upgrres1  29398  crctcshwlkn0lem2  29896  wwlksnred  29977  clwwlkccatlem  30076  clwwlkf  30134  wwlksubclwwlk  30145  eupth2lems  30325  sspmval  30820  sspimsval  30825  ubthlem1  30957  shsubcl  31307  shorth  31382  elspansn3  31659  elnlfn  32015  elpjrn  32277  sumdmdlem2  32506  nfpconfp  32721  xrofsup  32857  elrspunidl  33520  ressply1mon1p  33660  fldextrspunlsplem  33850  cmpcref  34027  zarclsiin  34048  cntmeas  34403  1stmbfm  34437  2ndmbfm  34438  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemodife  34675  ballotlemimin  34683  bnj1171  35175  bnj1280  35195  r1filimi  35278  subgrwlk  35345  gonarlem  35607  goalrlem  35609  mrsubrn  35726  elfzm12  35888  ontgval  36644  bj-restuni  37347  pibt2  37669  lindsenlbs  37863  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  itg2addnclem  37919  itg2addnclem2  37920  ftc1anclem7  37947  ismtyima  38051  suceldisj  39066  lshpkr  39490  psubatN  40128  elpaddn0  40173  pclfinN  40273  diael  41416  dia2dimlem12  41448  dicelval1stN  41561  dicelval2nd  41562  dib2dim  41616  dih2dimbALTN  41618  dihlspsnssN  41705  dvh1dim  41815  lcfrvalsnN  41914  mapdrvallem2  42018  mapdpglem2  42046  hdmap10lem  42212  hdmap11lem2  42215  hdmapoc  42304  primrootscoprbij  42469  primrootspoweq0  42473  aks6d1c2  42497  sticksstones3  42515  sticksstones17  42530  sticksstones18  42531  unitscyglem2  42563  unitscyglem4  42565  unitscyglem5  42566  isnacs3  43064  aomclem2  43409  kelac1  43417  rngunsnply  43523  safesnsupfiub  43769  intabssd  43872  iunrelexp0  44055  rfovcnvf1od  44357  rfovcnvfvd  44360  fsovrfovd  44362  clsk1indlem3  44396  neik0pk1imk0  44400  ntrneineine0lem  44436  ntrneiel2  44439  ntrneikb  44447  ntrneik4w  44453  mnuop3d  44624  dvconstbi  44687  expgrowth  44688  modelaxreplem2  45332  modelaxreplem3  45333  climsuselem1  45964  climsuse  45965  limcresiooub  45997  iblsplit  46321  iblspltprt  46328  stoweidlem62  46417  stirlinglem11  46439  fourierdlem41  46503  qndenserrnbllem  46649  sge0fodjrnlem  46771  smflimsuplem7  47181  fafvelcdm  47527  fafv2elcdm  47591  ceilhalfelfzo1  47687  smonoord  47728  iccpartiltu  47779  iccpartigtl  47780  iccpartiun  47791  iccpartdisj  47794  bgoldbtbndlem2  48163  gpgedgvtx1  48419  lidldomn1  48588  rhmsubcALTVlem4  48641  funcringcsetcALTV2lem9  48655  lincresunit3lem1  48836  setrec1  50047  setis  50054  vsetrec  50059  pgindnf  50072