Theorem sseld 3930

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2836  df-ss 3916

This theorem is used by:  sselda  3931  sseldd  3932  ssneld  3933  eqrrabd  4034  elelpwi  4567  ssbrd  5148  uniopel  5489  exopxfr2  5822  dmrnssfld  5956  preddowncl  6334  opelf  6741  elfvunirn  6913  fimarab  6957  fvimacnv  7050  ffvelcdm  7079  fnsnr  7166  f1imass  7266  onminex  7814  xpord2pred  8155  extmptsuppeq  8198  suppssr  8205  suppssrg  8206  dftpos3  8254  oa00  8560  omordi  8567  omlimcl  8579  omeulem1  8583  nnmordi  8633  mapsnd  8907  ixpf  8941  pw2f1olem  9093  pssnn  9177  findcard3  9267  ixpfi2  9332  fissuni  9339  elfiun  9415  dffi3  9416  supssd  9448  infssd  9479  ordiso2  9502  ordtypelem7  9511  ixpiunwdom  9577  inf3lem2  9623  cantnfp1lem3  9674  cantnfp1  9675  cantnflem1  9683  cantnf  9687  trcl  9722  r1ordg  9778  rankelb  9826  rankuni2b  9860  rankval4  9877  tcrank  9894  r1filimi  9896  cplem1  9943  cplem1OLD  9944  setrec1  9965  carduniima  10168  alephfp  10180  kmlem2  10223  isf32lem3  10426  domtriomlem  10513  axdc3lem2  10522  zorn2lem7  10573  ttukeylem6  10585  iundom2g  10617  fpwwe2lem12  10720  tskss  10836  tskhf  10846  inatsk  10856  gruss  10874  gruel  10881  grur1  10898  prlem934  11111  ltexprlem7  11120  supsr  11190  dedekind  11466  supadd  12278  supmullem2  12281  uzind  12784  iccsplit  13609  elfz0add  13753  predfz  13780  elfzoextl  13849  fsuppmapnn0fiub  14127  ccatval2  14716  swrdswrd  14847  pfxccatin12lem2a  14869  swrdccatin2  14871  pfxccatpfx2  14879  cshimadifsn0  14974  01sqrexlem6  15407  isercolllem2  15826  fsumcvg  15871  isumrpcl  16005  fprodcvg  16090  rpnnen2lem4  16378  fproddvdsd  16498  saddisj  16628  sadass  16634  bitsshft  16638  smuval2  16645  smupvallem  16646  smu01lem  16648  smueqlem  16653  reumodprminv  16975  ramub1lem1  17197  firest  17596  mrissmrid  17808  initoeu2lem0  18181  acsfiindd  18720  acsmapd  18721  dirge  18770  chndss  18783  issubmnd  18946  issubg2  19345  eqgid  19385  cyccom  19411  dprdff  20221  dprddisj2  20248  ablfac1c  20280  c0rnghm  20780  issubrng2  20803  subrgdvds  20831  issubrg2  20837  rnghmsscmap  20875  rngcsect  20881  funcrngcsetc  20885  rhmsscmap  20904  rhmsscrnghm  20910  ringcsect  20915  funcringcsetc  20919  rhmsubclem4  20933  lssssr  21222  lssats2  21268  lbspss  21350  lsmelval2  21353  lspprat  21424  lbsextlem2  21430  lbsextlem3  21431  rnglidlmmgm  21526  rnglidlmsgrp  21527  rnglidlrng  21528  df2idl2crng  21570  lpigen  21652  psgndiflemB  21899  lsmcss  21991  obselocv  22027  f1lindf  22121  lindsenlbs  22150  issubassa3  22167  mplcoe5lem  22341  mdetdiaglem  22906  cpmadugsumlemF  23187  toprntopon  23236  elcls  23384  clsndisj  23386  elcls3  23394  neindisj  23428  lpval  23450  lpsscls  23452  lpss3  23455  maxlp  23458  restntr  23493  ordtbas2  23502  ordtbas  23503  pnfnei  23531  mnfnei  23532  cncls2  23584  lmcnp  23615  lpcls  23675  hauscmplem  23717  2ndcdisj  23768  kgen2ss  23867  txuni2  23877  ptpjpre1  23883  tx1cn  23921  tx2cn  23922  prdstopn  23940  txlm  23960  imasnopn  24002  imasncld  24003  imasncls  24004  tgqtop  24024  regr1lem  24051  fgss2  24186  uzfbas  24210  ufilmax  24219  uffix2  24236  ufildr  24243  fmfnfmlem1  24266  fmco  24273  flimrest  24295  fclsopn  24326  fclscf  24337  flimfcls  24338  alexsubALTlem4  24362  qustgplem  24433  imasf1oxms  24801  prdsbl  24803  metrest  24836  iccntr  25134  reconnlem2  25140  caucfil  25597  caussi  25611  bcthlem5  25642  ovoliunlem1  25816  shft2rab  25822  sca2rab  25826  ovolicc2  25836  vitalilem2  25923  vitalilem5  25926  mbfinf  25979  i1f1lem  26003  mbfi1fseqlem4  26032  itgss  26125  itgcn  26158  c1liplem1  26309  c1lip1  26310  c1lip3  26312  ply1remlem  26476  plyconz  26624  plyexmo  26629  taylply2  26688  lgamucov  27358  fsumvma  27533  logfaclbnd  27542  ltsres  28012  nosepssdm  28036  nodenselem8  28041  nosupno  28053  nosupbday  28055  noinfbday  28070  elmade  28236  oldssmade  28246  mulsproplem13  28507  mulsproplem14  28508  precsexlem10  28595  bdayons  28655  uzsind  28784  axlowdimlem16  29528  axcontlem9  29543  edgupgr  29705  upgredg  29708  subgreldmiedg  29857  upgrres1  29887  subgrwlk  30262  crctcshwlkn0lem2  30393  wwlksnred  30474  clwwlkccatlem  30573  clwwlkf  30631  wwlksubclwwlk  30642  eupth2lems  30832  sspmval  31328  sspimsval  31333  ubthlem1  31465  shsubcl  31815  shorth  31890  elspansn3  32167  elnlfn  32523  elpjrn  32785  sumdmdlem2  33014  nfpconfp  33219  xrofsup  33352  elrspunidl  33971  ressply1mon1p  34093  fldextrspunlsplem  34298  cmpcref  34475  zarclsiin  34496  cntmeas  34852  1stmbfm  34885  2ndmbfm  34886  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemodife  35123  ballotlemimin  35131  bnj1171  35623  bnj1280  35643  gonarlem  36138  goalrlem  36140  mrsubrn  36257  elfzm12  36419  ontgval  37199  elttctr  37273  bj-restuni  37998  pibt2  38320  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  itg2addnclem  38569  itg2addnclem2  38570  ftc1anclem7  38597  ismtyima  38717  suceldisj  39730  lshpkr  40154  psubatN  40792  elpaddn0  40837  pclfinN  40937  diael  42080  dia2dimlem12  42112  dicelval1stN  42225  dicelval2nd  42226  dib2dim  42280  dih2dimbALTN  42282  dihlspsnssN  42369  dvh1dim  42479  lcfrvalsnN  42578  mapdrvallem2  42682  mapdpglem2  42710  hdmap10lem  42876  hdmap11lem2  42879  hdmapoc  42968  primrootscoprbij  43132  primrootspoweq0  43136  aks6d1c2  43160  sticksstones3  43178  sticksstones17  43193  sticksstones18  43194  unitscyglem2  43226  unitscyglem4  43228  unitscyglem5  43229  isnacs3  43700  aomclem2  44041  kelac1  44049  rngunsnply  44155  safesnsupfiub  44401  intabssd  44504  iunrelexp0  44687  rfovcnvf1od  44989  rfovcnvfvd  44992  fsovrfovd  44994  clsk1indlem3  45028  neik0pk1imk0  45032  ntrneineine0lem  45068  ntrneiel2  45071  ntrneikb  45079  ntrneik4w  45085  mnuop3d  45240  dvconstbi  45303  expgrowth  45304  modelaxreplem2  45947  modelaxreplem3  45948  climsuselem1  46588  climsuse  46589  limcresiooub  46621  iblsplit  46945  iblspltprt  46952  stoweidlem62  47041  stirlinglem11  47063  fourierdlem41  47127  qndenserrnbllem  47273  sge0fodjrnlem  47395  smflimsuplem7  47805  fafvelcdm  48209  fafv2elcdm  48273  ceilhalfelfzo1  48373  smonoord  48416  muldvdsfacm1  48426  iccpartiltu  48473  iccpartigtl  48474  iccpartiun  48485  iccpartdisj  48488  bgoldbtbndlem2  48873  gpgedgvtx1  49129  lidldomn1  49297  rhmsubcALTVlem4  49350  funcringcsetcALTV2lem9  49364  lincresunit3lem1  49560  setis  50760  vsetrec  50765  pgindnf  50778