Theorem sseld 3962

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

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

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 2810  df-ss 3948

This theorem is referenced by:  sselda  3963  sseldd  3964  ssneld  3965  eqrrabd  4066  elelpwi  4590  ssbrd  5167  uniopel  5496  exopxfr2  5829  dmrnssfld  5958  preddowncl  6326  opelf  6744  elfvunirn  6913  fimarab  6958  fvimacnv  7048  ffvelcdm  7076  fnsnr  7160  f1imass  7262  onminex  7801  xpord2pred  8149  extmptsuppeq  8192  suppssr  8199  suppssrg  8200  dftpos3  8248  wfrlem16OLD  8343  oa00  8576  omordi  8583  omlimcl  8595  omeulem1  8599  nnmordi  8648  mapsnd  8905  ixpf  8939  pw2f1olem  9095  pssnn  9187  findcard3  9295  findcard3OLD  9296  ixpfi2  9367  fissuni  9374  elfiun  9447  dffi3  9448  supssd  9480  infssd  9511  ordiso2  9534  ordtypelem7  9543  ixpiunwdom  9609  inf3lem2  9648  cantnfp1lem3  9699  cantnfp1  9700  cantnflem1  9708  cantnf  9712  trcl  9747  r1ordg  9797  rankelb  9843  rankuni2b  9872  rankval4  9886  tcrank  9903  cplem1  9908  carduniima  10115  alephfp  10127  kmlem2  10171  isf32lem3  10374  domtriomlem  10461  axdc3lem2  10470  zorn2lem7  10521  ttukeylem6  10533  iundom2g  10559  fpwwe2lem12  10661  tskss  10777  tskr1om2  10787  inatsk  10797  gruss  10815  gruel  10822  grur1  10839  prlem934  11052  ltexprlem7  11061  supsr  11131  dedekind  11403  supadd  12215  supmullem2  12218  uzind  12690  iccsplit  13507  elfz0add  13648  predfz  13675  elfzoextl  13742  fsuppmapnn0fiub  14014  ccatval2  14601  swrdswrd  14728  pfxccatin12lem2a  14750  swrdccatin2  14752  pfxccatpfx2  14760  cshimadifsn0  14854  01sqrexlem6  15271  isercolllem2  15687  fsumcvg  15733  isumrpcl  15864  fprodcvg  15951  rpnnen2lem4  16240  fproddvdsd  16359  saddisj  16489  sadass  16495  bitsshft  16499  smuval2  16506  smupvallem  16507  smu01lem  16509  smueqlem  16514  reumodprminv  16829  ramub1lem1  17051  firest  17451  mrissmrid  17658  initoeu2lem0  18031  acsfiindd  18568  acsmapd  18569  dirge  18618  issubmnd  18744  issubg2  19129  eqgid  19168  cyccom  19191  dprdff  20000  dprddisj2  20027  ablfac1c  20059  c0rnghm  20500  issubrng2  20523  subrgdvds  20551  issubrg2  20557  rnghmsscmap  20595  rngcsect  20601  funcrngcsetc  20605  rhmsscmap  20624  rhmsscrnghm  20630  ringcsect  20635  funcringcsetc  20639  rhmsubclem4  20653  lssssr  20916  lssats2  20962  lbspss  21045  lsmelval2  21048  lspprat  21119  lbsextlem2  21125  lbsextlem3  21126  rnglidlmmgm  21211  rnglidlmsgrp  21212  rnglidlrng  21213  lpigen  21301  psgndiflemB  21565  lsmcss  21657  obselocv  21693  f1lindf  21787  issubassa3  21831  mplcoe5lem  22002  mdetdiaglem  22541  cpmadugsumlemF  22819  toprntopon  22868  elcls  23016  clsndisj  23018  elcls3  23026  neindisj  23060  lpval  23082  lpsscls  23084  lpss3  23087  maxlp  23090  restntr  23125  ordtbas2  23134  ordtbas  23135  pnfnei  23163  mnfnei  23164  cncls2  23216  lmcnp  23247  lpcls  23307  hauscmplem  23349  2ndcdisj  23399  kgen2ss  23498  txuni2  23508  ptpjpre1  23514  tx1cn  23552  tx2cn  23553  prdstopn  23571  txlm  23591  imasnopn  23633  imasncld  23634  imasncls  23635  tgqtop  23655  regr1lem  23682  fgss2  23817  uzfbas  23841  ufilmax  23850  uffix2  23867  ufildr  23874  fmfnfmlem1  23897  fmco  23904  flimrest  23926  fclsopn  23957  fclscf  23968  flimfcls  23969  alexsubALTlem4  23993  qustgplem  24064  imasf1oxms  24433  prdsbl  24435  metrest  24468  iccntr  24766  reconnlem2  24772  caucfil  25240  caussi  25254  bcthlem5  25285  ovoliunlem1  25460  shft2rab  25466  sca2rab  25470  ovolicc2  25480  vitalilem2  25567  vitalilem5  25570  mbfinf  25623  i1f1lem  25647  mbfi1fseqlem4  25676  itgss  25770  itgcn  25803  c1liplem1  25958  c1lip1  25959  c1lip3  25961  ply1remlem  26127  plyexmo  26278  taylply2  26332  lgamucov  27005  fsumvma  27181  logfaclbnd  27190  sltres  27631  nosepssdm  27655  nodenselem8  27660  nosupno  27672  nosupbday  27674  noinfbday  27689  elmade  27836  oldssmade  27846  mulsproplem13  28088  mulsproplem14  28089  precsexlem10  28175  bdayon  28230  uzsind  28350  axlowdimlem16  28941  axcontlem9  28956  edgupgr  29118  upgredg  29121  subgreldmiedg  29267  upgrres1  29297  crctcshwlkn0lem2  29798  wwlksnred  29879  clwwlkccatlem  29975  clwwlkf  30033  wwlksubclwwlk  30044  eupth2lems  30224  sspmval  30719  sspimsval  30724  ubthlem1  30856  shsubcl  31206  shorth  31281  elspansn3  31558  elnlfn  31914  elpjrn  32176  sumdmdlem2  32405  nfpconfp  32615  xrofsup  32749  elrspunidl  33448  ressply1mon1p  33586  fldextrspunlsplem  33719  cmpcref  33886  zarclsiin  33907  cntmeas  34262  1stmbfm  34297  2ndmbfm  34298  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemodife  34535  ballotlemimin  34543  bnj1171  35036  bnj1280  35056  subgrwlk  35159  gonarlem  35421  goalrlem  35423  mrsubrn  35540  elfzm12  35702  ontgval  36454  bj-restuni  37120  pibt2  37440  lindsenlbs  37644  poimirlem29  37678  poimirlem30  37679  poimirlem31  37680  itg2addnclem  37700  itg2addnclem2  37701  ftc1anclem7  37728  ismtyima  37832  lshpkr  39140  psubatN  39779  elpaddn0  39824  pclfinN  39924  diael  41067  dia2dimlem12  41099  dicelval1stN  41212  dicelval2nd  41213  dib2dim  41267  dih2dimbALTN  41269  dihlspsnssN  41356  dvh1dim  41466  lcfrvalsnN  41565  mapdrvallem2  41669  mapdpglem2  41697  hdmap10lem  41863  hdmap11lem2  41866  hdmapoc  41955  primrootscoprbij  42120  primrootspoweq0  42124  aks6d1c2  42148  sticksstones3  42166  sticksstones17  42181  sticksstones18  42182  unitscyglem2  42214  unitscyglem4  42216  unitscyglem5  42217  isnacs3  42708  aomclem2  43054  kelac1  43062  rngunsnply  43168  safesnsupfiub  43415  intabssd  43518  iunrelexp0  43701  rfovcnvf1od  44003  rfovcnvfvd  44006  fsovrfovd  44008  clsk1indlem3  44042  neik0pk1imk0  44046  ntrneineine0lem  44082  ntrneiel2  44085  ntrneikb  44093  ntrneik4w  44099  mnuop3d  44270  dvconstbi  44333  expgrowth  44334  modelaxreplem2  44979  modelaxreplem3  44980  climsuselem1  45616  climsuse  45617  limcresiooub  45651  iblsplit  45975  iblspltprt  45982  stoweidlem62  46071  stirlinglem11  46093  fourierdlem41  46157  qndenserrnbllem  46303  sge0fodjrnlem  46425  smflimsuplem7  46835  fafvelcdm  47179  fafv2elcdm  47243  ceilhalfelfzo1  47339  smonoord  47365  iccpartiltu  47416  iccpartigtl  47417  iccpartiun  47428  iccpartdisj  47431  bgoldbtbndlem2  47800  gpgedgvtx1  48046  lidldomn1  48186  rhmsubcALTVlem4  48239  funcringcsetcALTV2lem9  48253  lincresunit3lem1  48435  setrec1  49535  setis  49542  vsetrec  49547  pgindnf  49560