Theorem sseld 3936

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

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

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 3922

This theorem is referenced by:  sselda  3937  sseldd  3938  ssneld  3939  eqrrabd  4039  elelpwi  4563  ssbrd  5138  uniopel  5463  exopxfr2  5791  dmrnssfld  5919  preddowncl  6284  opelf  6689  elfvunirn  6856  fimarab  6901  fvimacnv  6991  ffvelcdm  7019  fnsnr  7103  f1imass  7205  onminex  7742  xpord2pred  8085  extmptsuppeq  8128  suppssr  8135  suppssrg  8136  dftpos3  8184  oa00  8484  omordi  8491  omlimcl  8503  omeulem1  8507  nnmordi  8556  mapsnd  8820  ixpf  8854  pw2f1olem  9005  pssnn  9092  findcard3  9187  findcard3OLD  9188  ixpfi2  9259  fissuni  9266  elfiun  9339  dffi3  9340  supssd  9372  infssd  9403  ordiso2  9426  ordtypelem7  9435  ixpiunwdom  9501  inf3lem2  9544  cantnfp1lem3  9595  cantnfp1  9596  cantnflem1  9604  cantnf  9608  trcl  9643  r1ordg  9693  rankelb  9739  rankuni2b  9768  rankval4  9782  tcrank  9799  cplem1  9804  carduniima  10009  alephfp  10021  kmlem2  10065  isf32lem3  10268  domtriomlem  10355  axdc3lem2  10364  zorn2lem7  10415  ttukeylem6  10427  iundom2g  10453  fpwwe2lem12  10555  tskss  10671  tskr1om2  10681  inatsk  10691  gruss  10709  gruel  10716  grur1  10733  prlem934  10946  ltexprlem7  10955  supsr  11025  dedekind  11297  supadd  12111  supmullem2  12114  uzind  12586  iccsplit  13406  elfz0add  13547  predfz  13574  elfzoextl  13642  fsuppmapnn0fiub  13916  ccatval2  14503  swrdswrd  14629  pfxccatin12lem2a  14651  swrdccatin2  14653  pfxccatpfx2  14661  cshimadifsn0  14755  01sqrexlem6  15172  isercolllem2  15591  fsumcvg  15637  isumrpcl  15768  fprodcvg  15855  rpnnen2lem4  16144  fproddvdsd  16264  saddisj  16394  sadass  16400  bitsshft  16404  smuval2  16411  smupvallem  16412  smu01lem  16414  smueqlem  16419  reumodprminv  16734  ramub1lem1  16956  firest  17354  mrissmrid  17565  initoeu2lem0  17938  acsfiindd  18477  acsmapd  18478  dirge  18527  issubmnd  18653  issubg2  19038  eqgid  19077  cyccom  19100  dprdff  19911  dprddisj2  19938  ablfac1c  19970  c0rnghm  20438  issubrng2  20461  subrgdvds  20489  issubrg2  20495  rnghmsscmap  20533  rngcsect  20539  funcrngcsetc  20543  rhmsscmap  20562  rhmsscrnghm  20568  ringcsect  20573  funcringcsetc  20577  rhmsubclem4  20591  lssssr  20875  lssats2  20921  lbspss  21004  lsmelval2  21007  lspprat  21078  lbsextlem2  21084  lbsextlem3  21085  rnglidlmmgm  21170  rnglidlmsgrp  21171  rnglidlrng  21172  lpigen  21260  psgndiflemB  21525  lsmcss  21617  obselocv  21653  f1lindf  21747  issubassa3  21791  mplcoe5lem  21962  mdetdiaglem  22501  cpmadugsumlemF  22779  toprntopon  22828  elcls  22976  clsndisj  22978  elcls3  22986  neindisj  23020  lpval  23042  lpsscls  23044  lpss3  23047  maxlp  23050  restntr  23085  ordtbas2  23094  ordtbas  23095  pnfnei  23123  mnfnei  23124  cncls2  23176  lmcnp  23207  lpcls  23267  hauscmplem  23309  2ndcdisj  23359  kgen2ss  23458  txuni2  23468  ptpjpre1  23474  tx1cn  23512  tx2cn  23513  prdstopn  23531  txlm  23551  imasnopn  23593  imasncld  23594  imasncls  23595  tgqtop  23615  regr1lem  23642  fgss2  23777  uzfbas  23801  ufilmax  23810  uffix2  23827  ufildr  23834  fmfnfmlem1  23857  fmco  23864  flimrest  23886  fclsopn  23917  fclscf  23928  flimfcls  23929  alexsubALTlem4  23953  qustgplem  24024  imasf1oxms  24393  prdsbl  24395  metrest  24428  iccntr  24726  reconnlem2  24732  caucfil  25199  caussi  25213  bcthlem5  25244  ovoliunlem1  25419  shft2rab  25425  sca2rab  25429  ovolicc2  25439  vitalilem2  25526  vitalilem5  25529  mbfinf  25582  i1f1lem  25606  mbfi1fseqlem4  25635  itgss  25729  itgcn  25762  c1liplem1  25917  c1lip1  25918  c1lip3  25920  ply1remlem  26086  plyexmo  26237  taylply2  26291  lgamucov  26964  fsumvma  27140  logfaclbnd  27149  sltres  27590  nosepssdm  27614  nodenselem8  27619  nosupno  27631  nosupbday  27633  noinfbday  27648  elmade  27799  oldssmade  27809  mulsproplem13  28054  mulsproplem14  28055  precsexlem10  28141  bdayon  28196  uzsind  28316  axlowdimlem16  28920  axcontlem9  28935  edgupgr  29097  upgredg  29100  subgreldmiedg  29246  upgrres1  29276  crctcshwlkn0lem2  29774  wwlksnred  29855  clwwlkccatlem  29951  clwwlkf  30009  wwlksubclwwlk  30020  eupth2lems  30200  sspmval  30695  sspimsval  30700  ubthlem1  30832  shsubcl  31182  shorth  31257  elspansn3  31534  elnlfn  31890  elpjrn  32152  sumdmdlem2  32381  nfpconfp  32589  xrofsup  32723  elrspunidl  33378  ressply1mon1p  33516  fldextrspunlsplem  33647  cmpcref  33819  zarclsiin  33840  cntmeas  34195  1stmbfm  34230  2ndmbfm  34231  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemodife  34468  ballotlemimin  34476  bnj1171  34969  bnj1280  34989  subgrwlk  35107  gonarlem  35369  goalrlem  35371  mrsubrn  35488  elfzm12  35650  ontgval  36407  bj-restuni  37073  pibt2  37393  lindsenlbs  37597  poimirlem29  37631  poimirlem30  37632  poimirlem31  37633  itg2addnclem  37653  itg2addnclem2  37654  ftc1anclem7  37681  ismtyima  37785  lshpkr  39098  psubatN  39737  elpaddn0  39782  pclfinN  39882  diael  41025  dia2dimlem12  41057  dicelval1stN  41170  dicelval2nd  41171  dib2dim  41225  dih2dimbALTN  41227  dihlspsnssN  41314  dvh1dim  41424  lcfrvalsnN  41523  mapdrvallem2  41627  mapdpglem2  41655  hdmap10lem  41821  hdmap11lem2  41824  hdmapoc  41913  primrootscoprbij  42078  primrootspoweq0  42082  aks6d1c2  42106  sticksstones3  42124  sticksstones17  42139  sticksstones18  42140  unitscyglem2  42172  unitscyglem4  42174  unitscyglem5  42175  isnacs3  42686  aomclem2  43031  kelac1  43039  rngunsnply  43145  safesnsupfiub  43392  intabssd  43495  iunrelexp0  43678  rfovcnvf1od  43980  rfovcnvfvd  43983  fsovrfovd  43985  clsk1indlem3  44019  neik0pk1imk0  44023  ntrneineine0lem  44059  ntrneiel2  44062  ntrneikb  44070  ntrneik4w  44076  mnuop3d  44247  dvconstbi  44310  expgrowth  44311  modelaxreplem2  44956  modelaxreplem3  44957  climsuselem1  45592  climsuse  45593  limcresiooub  45627  iblsplit  45951  iblspltprt  45958  stoweidlem62  46047  stirlinglem11  46069  fourierdlem41  46133  qndenserrnbllem  46279  sge0fodjrnlem  46401  smflimsuplem7  46811  fafvelcdm  47158  fafv2elcdm  47222  ceilhalfelfzo1  47318  smonoord  47359  iccpartiltu  47410  iccpartigtl  47411  iccpartiun  47422  iccpartdisj  47425  bgoldbtbndlem2  47794  gpgedgvtx1  48050  lidldomn1  48219  rhmsubcALTVlem4  48272  funcringcsetcALTV2lem9  48286  lincresunit3lem1  48468  setrec1  49680  setis  49687  vsetrec  49692  pgindnf  49705