Theorem sseld 3928

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3897

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 2113

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

This theorem is referenced by:  sselda  3929  sseldd  3930  ssneld  3931  eqrrabd  4031  elelpwi  4555  ssbrd  5129  uniopel  5451  exopxfr2  5779  dmrnssfld  5908  preddowncl  6274  opelf  6679  elfvunirn  6847  fimarab  6891  fvimacnv  6981  ffvelcdm  7009  fnsnr  7092  f1imass  7193  onminex  7730  xpord2pred  8070  extmptsuppeq  8113  suppssr  8120  suppssrg  8121  dftpos3  8169  oa00  8469  omordi  8476  omlimcl  8488  omeulem1  8492  nnmordi  8541  mapsnd  8805  ixpf  8839  pw2f1olem  8989  pssnn  9073  findcard3  9162  ixpfi2  9229  fissuni  9236  elfiun  9309  dffi3  9310  supssd  9342  infssd  9373  ordiso2  9396  ordtypelem7  9405  ixpiunwdom  9471  inf3lem2  9514  cantnfp1lem3  9565  cantnfp1  9566  cantnflem1  9574  cantnf  9578  trcl  9613  r1ordg  9666  rankelb  9712  rankuni2b  9741  rankval4  9755  tcrank  9772  cplem1  9777  carduniima  9982  alephfp  9994  kmlem2  10038  isf32lem3  10241  domtriomlem  10328  axdc3lem2  10337  zorn2lem7  10388  ttukeylem6  10400  iundom2g  10426  fpwwe2lem12  10528  tskss  10644  tskr1om2  10654  inatsk  10664  gruss  10682  gruel  10689  grur1  10706  prlem934  10919  ltexprlem7  10928  supsr  10998  dedekind  11271  supadd  12085  supmullem2  12088  uzind  12560  iccsplit  13380  elfz0add  13521  predfz  13548  elfzoextl  13616  fsuppmapnn0fiub  13893  ccatval2  14480  swrdswrd  14607  pfxccatin12lem2a  14629  swrdccatin2  14631  pfxccatpfx2  14639  cshimadifsn0  14732  01sqrexlem6  15149  isercolllem2  15568  fsumcvg  15614  isumrpcl  15745  fprodcvg  15832  rpnnen2lem4  16121  fproddvdsd  16241  saddisj  16371  sadass  16377  bitsshft  16381  smuval2  16388  smupvallem  16389  smu01lem  16391  smueqlem  16396  reumodprminv  16711  ramub1lem1  16933  firest  17331  mrissmrid  17542  initoeu2lem0  17915  acsfiindd  18454  acsmapd  18455  dirge  18504  chndss  18517  issubmnd  18664  issubg2  19049  eqgid  19087  cyccom  19110  dprdff  19921  dprddisj2  19948  ablfac1c  19980  c0rnghm  20445  issubrng2  20468  subrgdvds  20496  issubrg2  20502  rnghmsscmap  20540  rngcsect  20546  funcrngcsetc  20550  rhmsscmap  20569  rhmsscrnghm  20575  ringcsect  20580  funcringcsetc  20584  rhmsubclem4  20598  lssssr  20882  lssats2  20928  lbspss  21011  lsmelval2  21014  lspprat  21085  lbsextlem2  21091  lbsextlem3  21092  rnglidlmmgm  21177  rnglidlmsgrp  21178  rnglidlrng  21179  lpigen  21267  psgndiflemB  21532  lsmcss  21624  obselocv  21660  f1lindf  21754  issubassa3  21798  mplcoe5lem  21969  mdetdiaglem  22508  cpmadugsumlemF  22786  toprntopon  22835  elcls  22983  clsndisj  22985  elcls3  22993  neindisj  23027  lpval  23049  lpsscls  23051  lpss3  23054  maxlp  23057  restntr  23092  ordtbas2  23101  ordtbas  23102  pnfnei  23130  mnfnei  23131  cncls2  23183  lmcnp  23214  lpcls  23274  hauscmplem  23316  2ndcdisj  23366  kgen2ss  23465  txuni2  23475  ptpjpre1  23481  tx1cn  23519  tx2cn  23520  prdstopn  23538  txlm  23558  imasnopn  23600  imasncld  23601  imasncls  23602  tgqtop  23622  regr1lem  23649  fgss2  23784  uzfbas  23808  ufilmax  23817  uffix2  23834  ufildr  23841  fmfnfmlem1  23864  fmco  23871  flimrest  23893  fclsopn  23924  fclscf  23935  flimfcls  23936  alexsubALTlem4  23960  qustgplem  24031  imasf1oxms  24399  prdsbl  24401  metrest  24434  iccntr  24732  reconnlem2  24738  caucfil  25205  caussi  25219  bcthlem5  25250  ovoliunlem1  25425  shft2rab  25431  sca2rab  25435  ovolicc2  25445  vitalilem2  25532  vitalilem5  25535  mbfinf  25588  i1f1lem  25612  mbfi1fseqlem4  25641  itgss  25735  itgcn  25768  c1liplem1  25923  c1lip1  25924  c1lip3  25926  ply1remlem  26092  plyexmo  26243  taylply2  26297  lgamucov  26970  fsumvma  27146  logfaclbnd  27155  sltres  27596  nosepssdm  27620  nodenselem8  27625  nosupno  27637  nosupbday  27639  noinfbday  27654  elmade  27807  oldssmade  27817  mulsproplem13  28062  mulsproplem14  28063  precsexlem10  28149  bdayon  28204  uzsind  28324  axlowdimlem16  28930  axcontlem9  28945  edgupgr  29107  upgredg  29110  subgreldmiedg  29256  upgrres1  29286  crctcshwlkn0lem2  29784  wwlksnred  29865  clwwlkccatlem  29961  clwwlkf  30019  wwlksubclwwlk  30030  eupth2lems  30210  sspmval  30705  sspimsval  30710  ubthlem1  30842  shsubcl  31192  shorth  31267  elspansn3  31544  elnlfn  31900  elpjrn  32162  sumdmdlem2  32391  nfpconfp  32606  xrofsup  32742  elrspunidl  33385  ressply1mon1p  33523  fldextrspunlsplem  33678  cmpcref  33855  zarclsiin  33876  cntmeas  34231  1stmbfm  34265  2ndmbfm  34266  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemodife  34503  ballotlemimin  34511  bnj1171  35004  bnj1280  35024  r1filimi  35106  subgrwlk  35168  gonarlem  35430  goalrlem  35432  mrsubrn  35549  elfzm12  35711  ontgval  36465  bj-restuni  37131  pibt2  37451  lindsenlbs  37655  poimirlem29  37689  poimirlem30  37690  poimirlem31  37691  itg2addnclem  37711  itg2addnclem2  37712  ftc1anclem7  37739  ismtyima  37843  lshpkr  39156  psubatN  39794  elpaddn0  39839  pclfinN  39939  diael  41082  dia2dimlem12  41114  dicelval1stN  41227  dicelval2nd  41228  dib2dim  41282  dih2dimbALTN  41284  dihlspsnssN  41371  dvh1dim  41481  lcfrvalsnN  41580  mapdrvallem2  41684  mapdpglem2  41712  hdmap10lem  41878  hdmap11lem2  41881  hdmapoc  41970  primrootscoprbij  42135  primrootspoweq0  42139  aks6d1c2  42163  sticksstones3  42181  sticksstones17  42196  sticksstones18  42197  unitscyglem2  42229  unitscyglem4  42231  unitscyglem5  42232  isnacs3  42743  aomclem2  43088  kelac1  43096  rngunsnply  43202  safesnsupfiub  43449  intabssd  43552  iunrelexp0  43735  rfovcnvf1od  44037  rfovcnvfvd  44040  fsovrfovd  44042  clsk1indlem3  44076  neik0pk1imk0  44080  ntrneineine0lem  44116  ntrneiel2  44119  ntrneikb  44127  ntrneik4w  44133  mnuop3d  44304  dvconstbi  44367  expgrowth  44368  modelaxreplem2  45012  modelaxreplem3  45013  climsuselem1  45647  climsuse  45648  limcresiooub  45680  iblsplit  46004  iblspltprt  46011  stoweidlem62  46100  stirlinglem11  46122  fourierdlem41  46186  qndenserrnbllem  46332  sge0fodjrnlem  46454  smflimsuplem7  46864  fafvelcdm  47201  fafv2elcdm  47265  ceilhalfelfzo1  47361  smonoord  47402  iccpartiltu  47453  iccpartigtl  47454  iccpartiun  47465  iccpartdisj  47468  bgoldbtbndlem2  47837  gpgedgvtx1  48093  lidldomn1  48262  rhmsubcALTVlem4  48315  funcringcsetcALTV2lem9  48329  lincresunit3lem1  48511  setrec1  49723  setis  49730  vsetrec  49735  pgindnf  49748