Theorem sseld 3945

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

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

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 3931

This theorem is referenced by:  sselda  3946  sseldd  3947  ssneld  3948  eqrrabd  4049  elelpwi  4573  ssbrd  5150  uniopel  5476  exopxfr2  5808  dmrnssfld  5937  preddowncl  6305  opelf  6721  elfvunirn  6890  fimarab  6935  fvimacnv  7025  ffvelcdm  7053  fnsnr  7137  f1imass  7239  onminex  7778  xpord2pred  8124  extmptsuppeq  8167  suppssr  8174  suppssrg  8175  dftpos3  8223  oa00  8523  omordi  8530  omlimcl  8542  omeulem1  8546  nnmordi  8595  mapsnd  8859  ixpf  8893  pw2f1olem  9045  pssnn  9132  findcard3  9229  findcard3OLD  9230  ixpfi2  9301  fissuni  9308  elfiun  9381  dffi3  9382  supssd  9414  infssd  9445  ordiso2  9468  ordtypelem7  9477  ixpiunwdom  9543  inf3lem2  9582  cantnfp1lem3  9633  cantnfp1  9634  cantnflem1  9642  cantnf  9646  trcl  9681  r1ordg  9731  rankelb  9777  rankuni2b  9806  rankval4  9820  tcrank  9837  cplem1  9842  carduniima  10049  alephfp  10061  kmlem2  10105  isf32lem3  10308  domtriomlem  10395  axdc3lem2  10404  zorn2lem7  10455  ttukeylem6  10467  iundom2g  10493  fpwwe2lem12  10595  tskss  10711  tskr1om2  10721  inatsk  10731  gruss  10749  gruel  10756  grur1  10773  prlem934  10986  ltexprlem7  10995  supsr  11065  dedekind  11337  supadd  12151  supmullem2  12154  uzind  12626  iccsplit  13446  elfz0add  13587  predfz  13614  elfzoextl  13682  fsuppmapnn0fiub  13956  ccatval2  14543  swrdswrd  14670  pfxccatin12lem2a  14692  swrdccatin2  14694  pfxccatpfx2  14702  cshimadifsn0  14796  01sqrexlem6  15213  isercolllem2  15632  fsumcvg  15678  isumrpcl  15809  fprodcvg  15896  rpnnen2lem4  16185  fproddvdsd  16305  saddisj  16435  sadass  16441  bitsshft  16445  smuval2  16452  smupvallem  16453  smu01lem  16455  smueqlem  16460  reumodprminv  16775  ramub1lem1  16997  firest  17395  mrissmrid  17602  initoeu2lem0  17975  acsfiindd  18512  acsmapd  18513  dirge  18562  issubmnd  18688  issubg2  19073  eqgid  19112  cyccom  19135  dprdff  19944  dprddisj2  19971  ablfac1c  20003  c0rnghm  20444  issubrng2  20467  subrgdvds  20495  issubrg2  20501  rnghmsscmap  20539  rngcsect  20545  funcrngcsetc  20549  rhmsscmap  20568  rhmsscrnghm  20574  ringcsect  20579  funcringcsetc  20583  rhmsubclem4  20597  lssssr  20860  lssats2  20906  lbspss  20989  lsmelval2  20992  lspprat  21063  lbsextlem2  21069  lbsextlem3  21070  rnglidlmmgm  21155  rnglidlmsgrp  21156  rnglidlrng  21157  lpigen  21245  psgndiflemB  21509  lsmcss  21601  obselocv  21637  f1lindf  21731  issubassa3  21775  mplcoe5lem  21946  mdetdiaglem  22485  cpmadugsumlemF  22763  toprntopon  22812  elcls  22960  clsndisj  22962  elcls3  22970  neindisj  23004  lpval  23026  lpsscls  23028  lpss3  23031  maxlp  23034  restntr  23069  ordtbas2  23078  ordtbas  23079  pnfnei  23107  mnfnei  23108  cncls2  23160  lmcnp  23191  lpcls  23251  hauscmplem  23293  2ndcdisj  23343  kgen2ss  23442  txuni2  23452  ptpjpre1  23458  tx1cn  23496  tx2cn  23497  prdstopn  23515  txlm  23535  imasnopn  23577  imasncld  23578  imasncls  23579  tgqtop  23599  regr1lem  23626  fgss2  23761  uzfbas  23785  ufilmax  23794  uffix2  23811  ufildr  23818  fmfnfmlem1  23841  fmco  23848  flimrest  23870  fclsopn  23901  fclscf  23912  flimfcls  23913  alexsubALTlem4  23937  qustgplem  24008  imasf1oxms  24377  prdsbl  24379  metrest  24412  iccntr  24710  reconnlem2  24716  caucfil  25183  caussi  25197  bcthlem5  25228  ovoliunlem1  25403  shft2rab  25409  sca2rab  25413  ovolicc2  25423  vitalilem2  25510  vitalilem5  25513  mbfinf  25566  i1f1lem  25590  mbfi1fseqlem4  25619  itgss  25713  itgcn  25746  c1liplem1  25901  c1lip1  25902  c1lip3  25904  ply1remlem  26070  plyexmo  26221  taylply2  26275  lgamucov  26948  fsumvma  27124  logfaclbnd  27133  sltres  27574  nosepssdm  27598  nodenselem8  27603  nosupno  27615  nosupbday  27617  noinfbday  27632  elmade  27779  oldssmade  27789  mulsproplem13  28031  mulsproplem14  28032  precsexlem10  28118  bdayon  28173  uzsind  28293  axlowdimlem16  28884  axcontlem9  28899  edgupgr  29061  upgredg  29064  subgreldmiedg  29210  upgrres1  29240  crctcshwlkn0lem2  29741  wwlksnred  29822  clwwlkccatlem  29918  clwwlkf  29976  wwlksubclwwlk  29987  eupth2lems  30167  sspmval  30662  sspimsval  30667  ubthlem1  30799  shsubcl  31149  shorth  31224  elspansn3  31501  elnlfn  31857  elpjrn  32119  sumdmdlem2  32348  nfpconfp  32556  xrofsup  32690  elrspunidl  33399  ressply1mon1p  33537  fldextrspunlsplem  33668  cmpcref  33840  zarclsiin  33861  cntmeas  34216  1stmbfm  34251  2ndmbfm  34252  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemodife  34489  ballotlemimin  34497  bnj1171  34990  bnj1280  35010  subgrwlk  35119  gonarlem  35381  goalrlem  35383  mrsubrn  35500  elfzm12  35662  ontgval  36419  bj-restuni  37085  pibt2  37405  lindsenlbs  37609  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  itg2addnclem  37665  itg2addnclem2  37666  ftc1anclem7  37693  ismtyima  37797  lshpkr  39110  psubatN  39749  elpaddn0  39794  pclfinN  39894  diael  41037  dia2dimlem12  41069  dicelval1stN  41182  dicelval2nd  41183  dib2dim  41237  dih2dimbALTN  41239  dihlspsnssN  41326  dvh1dim  41436  lcfrvalsnN  41535  mapdrvallem2  41639  mapdpglem2  41667  hdmap10lem  41833  hdmap11lem2  41836  hdmapoc  41925  primrootscoprbij  42090  primrootspoweq0  42094  aks6d1c2  42118  sticksstones3  42136  sticksstones17  42151  sticksstones18  42152  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  isnacs3  42698  aomclem2  43044  kelac1  43052  rngunsnply  43158  safesnsupfiub  43405  intabssd  43508  iunrelexp0  43691  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  clsk1indlem3  44032  neik0pk1imk0  44036  ntrneineine0lem  44072  ntrneiel2  44075  ntrneikb  44083  ntrneik4w  44089  mnuop3d  44260  dvconstbi  44323  expgrowth  44324  modelaxreplem2  44969  modelaxreplem3  44970  climsuselem1  45605  climsuse  45606  limcresiooub  45640  iblsplit  45964  iblspltprt  45971  stoweidlem62  46060  stirlinglem11  46082  fourierdlem41  46146  qndenserrnbllem  46292  sge0fodjrnlem  46414  smflimsuplem7  46824  fafvelcdm  47171  fafv2elcdm  47235  ceilhalfelfzo1  47331  smonoord  47372  iccpartiltu  47423  iccpartigtl  47424  iccpartiun  47435  iccpartdisj  47438  bgoldbtbndlem2  47807  gpgedgvtx1  48053  lidldomn1  48219  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem9  48286  lincresunit3lem1  48468  setrec1  49680  setis  49687  vsetrec  49692  pgindnf  49705