Theorem sseld 3932

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

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

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 2811  df-ss 3918

This theorem is referenced by:  sselda  3933  sseldd  3934  ssneld  3935  eqrrabd  4038  elelpwi  4564  ssbrd  5141  uniopel  5464  exopxfr2  5793  dmrnssfld  5923  preddowncl  6290  opelf  6695  elfvunirn  6864  fimarab  6908  fvimacnv  6998  ffvelcdm  7026  fnsnr  7109  f1imass  7210  onminex  7747  xpord2pred  8087  extmptsuppeq  8130  suppssr  8137  suppssrg  8138  dftpos3  8186  oa00  8486  omordi  8493  omlimcl  8505  omeulem1  8509  nnmordi  8559  mapsnd  8824  ixpf  8858  pw2f1olem  9009  pssnn  9093  findcard3  9183  ixpfi2  9250  fissuni  9257  elfiun  9333  dffi3  9334  supssd  9366  infssd  9397  ordiso2  9420  ordtypelem7  9429  ixpiunwdom  9495  inf3lem2  9538  cantnfp1lem3  9589  cantnfp1  9590  cantnflem1  9598  cantnf  9602  trcl  9637  r1ordg  9690  rankelb  9736  rankuni2b  9765  rankval4  9779  tcrank  9796  cplem1  9801  carduniima  10006  alephfp  10018  kmlem2  10062  isf32lem3  10265  domtriomlem  10352  axdc3lem2  10361  zorn2lem7  10412  ttukeylem6  10424  iundom2g  10450  fpwwe2lem12  10553  tskss  10669  tskr1om2  10679  inatsk  10689  gruss  10707  gruel  10714  grur1  10731  prlem934  10944  ltexprlem7  10953  supsr  11023  dedekind  11296  supadd  12110  supmullem2  12113  uzind  12584  iccsplit  13401  elfz0add  13542  predfz  13569  elfzoextl  13637  fsuppmapnn0fiub  13914  ccatval2  14501  swrdswrd  14628  pfxccatin12lem2a  14650  swrdccatin2  14652  pfxccatpfx2  14660  cshimadifsn0  14753  01sqrexlem6  15170  isercolllem2  15589  fsumcvg  15635  isumrpcl  15766  fprodcvg  15853  rpnnen2lem4  16142  fproddvdsd  16262  saddisj  16392  sadass  16398  bitsshft  16402  smuval2  16409  smupvallem  16410  smu01lem  16412  smueqlem  16417  reumodprminv  16732  ramub1lem1  16954  firest  17352  mrissmrid  17564  initoeu2lem0  17937  acsfiindd  18476  acsmapd  18477  dirge  18526  chndss  18539  issubmnd  18686  issubg2  19071  eqgid  19109  cyccom  19132  dprdff  19943  dprddisj2  19970  ablfac1c  20002  c0rnghm  20468  issubrng2  20491  subrgdvds  20519  issubrg2  20525  rnghmsscmap  20563  rngcsect  20569  funcrngcsetc  20573  rhmsscmap  20592  rhmsscrnghm  20598  ringcsect  20603  funcringcsetc  20607  rhmsubclem4  20621  lssssr  20905  lssats2  20951  lbspss  21034  lsmelval2  21037  lspprat  21108  lbsextlem2  21114  lbsextlem3  21115  rnglidlmmgm  21200  rnglidlmsgrp  21201  rnglidlrng  21202  lpigen  21290  psgndiflemB  21555  lsmcss  21647  obselocv  21683  f1lindf  21777  issubassa3  21821  mplcoe5lem  21994  mdetdiaglem  22542  cpmadugsumlemF  22820  toprntopon  22869  elcls  23017  clsndisj  23019  elcls3  23027  neindisj  23061  lpval  23083  lpsscls  23085  lpss3  23088  maxlp  23091  restntr  23126  ordtbas2  23135  ordtbas  23136  pnfnei  23164  mnfnei  23165  cncls2  23217  lmcnp  23248  lpcls  23308  hauscmplem  23350  2ndcdisj  23400  kgen2ss  23499  txuni2  23509  ptpjpre1  23515  tx1cn  23553  tx2cn  23554  prdstopn  23572  txlm  23592  imasnopn  23634  imasncld  23635  imasncls  23636  tgqtop  23656  regr1lem  23683  fgss2  23818  uzfbas  23842  ufilmax  23851  uffix2  23868  ufildr  23875  fmfnfmlem1  23898  fmco  23905  flimrest  23927  fclsopn  23958  fclscf  23969  flimfcls  23970  alexsubALTlem4  23994  qustgplem  24065  imasf1oxms  24433  prdsbl  24435  metrest  24468  iccntr  24766  reconnlem2  24772  caucfil  25239  caussi  25253  bcthlem5  25284  ovoliunlem1  25459  shft2rab  25465  sca2rab  25469  ovolicc2  25479  vitalilem2  25566  vitalilem5  25569  mbfinf  25622  i1f1lem  25646  mbfi1fseqlem4  25675  itgss  25769  itgcn  25802  c1liplem1  25957  c1lip1  25958  c1lip3  25960  ply1remlem  26126  plyexmo  26277  taylply2  26331  lgamucov  27004  fsumvma  27180  logfaclbnd  27189  ltsres  27630  nosepssdm  27654  nodenselem8  27659  nosupno  27671  nosupbday  27673  noinfbday  27688  elmade  27853  oldssmade  27863  mulsproplem13  28124  mulsproplem14  28125  precsexlem10  28212  bdayons  28272  uzsind  28401  axlowdimlem16  29030  axcontlem9  29045  edgupgr  29207  upgredg  29210  subgreldmiedg  29356  upgrres1  29386  crctcshwlkn0lem2  29884  wwlksnred  29965  clwwlkccatlem  30064  clwwlkf  30122  wwlksubclwwlk  30133  eupth2lems  30313  sspmval  30808  sspimsval  30813  ubthlem1  30945  shsubcl  31295  shorth  31370  elspansn3  31647  elnlfn  32003  elpjrn  32265  sumdmdlem2  32494  nfpconfp  32710  xrofsup  32847  elrspunidl  33509  ressply1mon1p  33649  fldextrspunlsplem  33830  cmpcref  34007  zarclsiin  34028  cntmeas  34383  1stmbfm  34417  2ndmbfm  34418  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemodife  34655  ballotlemimin  34663  bnj1171  35156  bnj1280  35176  r1filimi  35259  subgrwlk  35326  gonarlem  35588  goalrlem  35590  mrsubrn  35707  elfzm12  35869  ontgval  36625  bj-restuni  37302  pibt2  37622  lindsenlbs  37816  poimirlem29  37850  poimirlem30  37851  poimirlem31  37852  itg2addnclem  37872  itg2addnclem2  37873  ftc1anclem7  37900  ismtyima  38004  lshpkr  39377  psubatN  40015  elpaddn0  40060  pclfinN  40160  diael  41303  dia2dimlem12  41335  dicelval1stN  41448  dicelval2nd  41449  dib2dim  41503  dih2dimbALTN  41505  dihlspsnssN  41592  dvh1dim  41702  lcfrvalsnN  41801  mapdrvallem2  41905  mapdpglem2  41933  hdmap10lem  42099  hdmap11lem2  42102  hdmapoc  42191  primrootscoprbij  42356  primrootspoweq0  42360  aks6d1c2  42384  sticksstones3  42402  sticksstones17  42417  sticksstones18  42418  unitscyglem2  42450  unitscyglem4  42452  unitscyglem5  42453  isnacs3  42952  aomclem2  43297  kelac1  43305  rngunsnply  43411  safesnsupfiub  43657  intabssd  43760  iunrelexp0  43943  rfovcnvf1od  44245  rfovcnvfvd  44248  fsovrfovd  44250  clsk1indlem3  44284  neik0pk1imk0  44288  ntrneineine0lem  44324  ntrneiel2  44327  ntrneikb  44335  ntrneik4w  44341  mnuop3d  44512  dvconstbi  44575  expgrowth  44576  modelaxreplem2  45220  modelaxreplem3  45221  climsuselem1  45853  climsuse  45854  limcresiooub  45886  iblsplit  46210  iblspltprt  46217  stoweidlem62  46306  stirlinglem11  46328  fourierdlem41  46392  qndenserrnbllem  46538  sge0fodjrnlem  46660  smflimsuplem7  47070  fafvelcdm  47416  fafv2elcdm  47480  ceilhalfelfzo1  47576  smonoord  47617  iccpartiltu  47668  iccpartigtl  47669  iccpartiun  47680  iccpartdisj  47683  bgoldbtbndlem2  48052  gpgedgvtx1  48308  lidldomn1  48477  rhmsubcALTVlem4  48530  funcringcsetcALTV2lem9  48544  lincresunit3lem1  48725  setrec1  49936  setis  49943  vsetrec  49948  pgindnf  49961