Theorem sseld 3929

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

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

This theorem is referenced by:  sselda  3930  sseldd  3931  ssneld  3932  eqrrabd  4035  elelpwi  4561  ssbrd  5138  uniopel  5461  exopxfr2  5790  dmrnssfld  5920  preddowncl  6287  opelf  6692  elfvunirn  6861  fimarab  6905  fvimacnv  6995  ffvelcdm  7023  fnsnr  7106  f1imass  7207  onminex  7744  xpord2pred  8084  extmptsuppeq  8127  suppssr  8134  suppssrg  8135  dftpos3  8183  oa00  8483  omordi  8490  omlimcl  8502  omeulem1  8506  nnmordi  8555  mapsnd  8820  ixpf  8854  pw2f1olem  9005  pssnn  9089  findcard3  9178  ixpfi2  9245  fissuni  9252  elfiun  9325  dffi3  9326  supssd  9358  infssd  9389  ordiso2  9412  ordtypelem7  9421  ixpiunwdom  9487  inf3lem2  9530  cantnfp1lem3  9581  cantnfp1  9582  cantnflem1  9590  cantnf  9594  trcl  9629  r1ordg  9682  rankelb  9728  rankuni2b  9757  rankval4  9771  tcrank  9788  cplem1  9793  carduniima  9998  alephfp  10010  kmlem2  10054  isf32lem3  10257  domtriomlem  10344  axdc3lem2  10353  zorn2lem7  10404  ttukeylem6  10416  iundom2g  10442  fpwwe2lem12  10544  tskss  10660  tskr1om2  10670  inatsk  10680  gruss  10698  gruel  10705  grur1  10722  prlem934  10935  ltexprlem7  10944  supsr  11014  dedekind  11287  supadd  12101  supmullem2  12104  uzind  12575  iccsplit  13392  elfz0add  13533  predfz  13560  elfzoextl  13628  fsuppmapnn0fiub  13905  ccatval2  14492  swrdswrd  14619  pfxccatin12lem2a  14641  swrdccatin2  14643  pfxccatpfx2  14651  cshimadifsn0  14744  01sqrexlem6  15161  isercolllem2  15580  fsumcvg  15626  isumrpcl  15757  fprodcvg  15844  rpnnen2lem4  16133  fproddvdsd  16253  saddisj  16383  sadass  16389  bitsshft  16393  smuval2  16400  smupvallem  16401  smu01lem  16403  smueqlem  16408  reumodprminv  16723  ramub1lem1  16945  firest  17343  mrissmrid  17555  initoeu2lem0  17928  acsfiindd  18467  acsmapd  18468  dirge  18517  chndss  18530  issubmnd  18677  issubg2  19062  eqgid  19100  cyccom  19123  dprdff  19934  dprddisj2  19961  ablfac1c  19993  c0rnghm  20459  issubrng2  20482  subrgdvds  20510  issubrg2  20516  rnghmsscmap  20554  rngcsect  20560  funcrngcsetc  20564  rhmsscmap  20583  rhmsscrnghm  20589  ringcsect  20594  funcringcsetc  20598  rhmsubclem4  20612  lssssr  20896  lssats2  20942  lbspss  21025  lsmelval2  21028  lspprat  21099  lbsextlem2  21105  lbsextlem3  21106  rnglidlmmgm  21191  rnglidlmsgrp  21192  rnglidlrng  21193  lpigen  21281  psgndiflemB  21546  lsmcss  21638  obselocv  21674  f1lindf  21768  issubassa3  21812  mplcoe5lem  21985  mdetdiaglem  22533  cpmadugsumlemF  22811  toprntopon  22860  elcls  23008  clsndisj  23010  elcls3  23018  neindisj  23052  lpval  23074  lpsscls  23076  lpss3  23079  maxlp  23082  restntr  23117  ordtbas2  23126  ordtbas  23127  pnfnei  23155  mnfnei  23156  cncls2  23208  lmcnp  23239  lpcls  23299  hauscmplem  23341  2ndcdisj  23391  kgen2ss  23490  txuni2  23500  ptpjpre1  23506  tx1cn  23544  tx2cn  23545  prdstopn  23563  txlm  23583  imasnopn  23625  imasncld  23626  imasncls  23627  tgqtop  23647  regr1lem  23674  fgss2  23809  uzfbas  23833  ufilmax  23842  uffix2  23859  ufildr  23866  fmfnfmlem1  23889  fmco  23896  flimrest  23918  fclsopn  23949  fclscf  23960  flimfcls  23961  alexsubALTlem4  23985  qustgplem  24056  imasf1oxms  24424  prdsbl  24426  metrest  24459  iccntr  24757  reconnlem2  24763  caucfil  25230  caussi  25244  bcthlem5  25275  ovoliunlem1  25450  shft2rab  25456  sca2rab  25460  ovolicc2  25470  vitalilem2  25557  vitalilem5  25560  mbfinf  25613  i1f1lem  25637  mbfi1fseqlem4  25666  itgss  25760  itgcn  25793  c1liplem1  25948  c1lip1  25949  c1lip3  25951  ply1remlem  26117  plyexmo  26268  taylply2  26322  lgamucov  26995  fsumvma  27171  logfaclbnd  27180  sltres  27621  nosepssdm  27645  nodenselem8  27650  nosupno  27662  nosupbday  27664  noinfbday  27679  elmade  27832  oldssmade  27842  mulsproplem13  28087  mulsproplem14  28088  precsexlem10  28174  bdayon  28229  uzsind  28349  axlowdimlem16  28956  axcontlem9  28971  edgupgr  29133  upgredg  29136  subgreldmiedg  29282  upgrres1  29312  crctcshwlkn0lem2  29810  wwlksnred  29891  clwwlkccatlem  29990  clwwlkf  30048  wwlksubclwwlk  30059  eupth2lems  30239  sspmval  30734  sspimsval  30739  ubthlem1  30871  shsubcl  31221  shorth  31296  elspansn3  31573  elnlfn  31929  elpjrn  32191  sumdmdlem2  32420  nfpconfp  32636  xrofsup  32775  elrspunidl  33437  ressply1mon1p  33577  fldextrspunlsplem  33758  cmpcref  33935  zarclsiin  33956  cntmeas  34311  1stmbfm  34345  2ndmbfm  34346  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemodife  34583  ballotlemimin  34591  bnj1171  35084  bnj1280  35104  r1filimi  35186  subgrwlk  35248  gonarlem  35510  goalrlem  35512  mrsubrn  35629  elfzm12  35791  ontgval  36547  bj-restuni  37214  pibt2  37534  lindsenlbs  37728  poimirlem29  37762  poimirlem30  37763  poimirlem31  37764  itg2addnclem  37784  itg2addnclem2  37785  ftc1anclem7  37812  ismtyima  37916  lshpkr  39289  psubatN  39927  elpaddn0  39972  pclfinN  40072  diael  41215  dia2dimlem12  41247  dicelval1stN  41360  dicelval2nd  41361  dib2dim  41415  dih2dimbALTN  41417  dihlspsnssN  41504  dvh1dim  41614  lcfrvalsnN  41713  mapdrvallem2  41817  mapdpglem2  41845  hdmap10lem  42011  hdmap11lem2  42014  hdmapoc  42103  primrootscoprbij  42268  primrootspoweq0  42272  aks6d1c2  42296  sticksstones3  42314  sticksstones17  42329  sticksstones18  42330  unitscyglem2  42362  unitscyglem4  42364  unitscyglem5  42365  isnacs3  42867  aomclem2  43212  kelac1  43220  rngunsnply  43326  safesnsupfiub  43573  intabssd  43676  iunrelexp0  43859  rfovcnvf1od  44161  rfovcnvfvd  44164  fsovrfovd  44166  clsk1indlem3  44200  neik0pk1imk0  44204  ntrneineine0lem  44240  ntrneiel2  44243  ntrneikb  44251  ntrneik4w  44257  mnuop3d  44428  dvconstbi  44491  expgrowth  44492  modelaxreplem2  45136  modelaxreplem3  45137  climsuselem1  45769  climsuse  45770  limcresiooub  45802  iblsplit  46126  iblspltprt  46133  stoweidlem62  46222  stirlinglem11  46244  fourierdlem41  46308  qndenserrnbllem  46454  sge0fodjrnlem  46576  smflimsuplem7  46986  fafvelcdm  47332  fafv2elcdm  47396  ceilhalfelfzo1  47492  smonoord  47533  iccpartiltu  47584  iccpartigtl  47585  iccpartiun  47596  iccpartdisj  47599  bgoldbtbndlem2  47968  gpgedgvtx1  48224  lidldomn1  48393  rhmsubcALTVlem4  48446  funcringcsetcALTV2lem9  48460  lincresunit3lem1  48641  setrec1  49852  setis  49859  vsetrec  49864  pgindnf  49877