Theorem sseld 3933

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

Syntax hints:   → wi 4   ∈ wcel 2141   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836  df-ss 3919

This theorem is referenced by:  sselda  3934  sseldd  3935  ssneld  3936  eqrrabd  4037  elelpwi  4562  ssbrd  5140  uniopel  5482  exopxfr2  5812  dmrnssfld  5946  preddowncl  6314  opelf  6720  elfvunirn  6892  fimarab  6936  fvimacnv  7029  ffvelcdm  7057  fnsnr  7142  f1imass  7243  onminex  7780  xpord2pred  8119  extmptsuppeq  8162  suppssr  8169  suppssrg  8170  dftpos3  8218  oa00  8522  omordi  8529  omlimcl  8541  omeulem1  8545  nnmordi  8595  mapsnd  8862  ixpf  8896  pw2f1olem  9047  pssnn  9131  findcard3  9221  ixpfi2  9287  fissuni  9294  elfiun  9370  dffi3  9371  supssd  9403  infssd  9434  ordiso2  9457  ordtypelem7  9466  ixpiunwdom  9532  inf3lem2  9578  cantnfp1lem3  9629  cantnfp1  9630  cantnflem1  9638  cantnf  9642  trcl  9677  r1ordg  9730  rankelb  9776  rankuni2b  9805  rankval4  9819  tcrank  9836  cplem1  9841  carduniima  10046  alephfp  10058  kmlem2  10102  isf32lem3  10306  domtriomlem  10393  axdc3lem2  10402  zorn2lem7  10453  ttukeylem6  10465  iundom2g  10491  fpwwe2lem12  10594  tskss  10710  tskr1om2  10720  inatsk  10730  gruss  10748  gruel  10755  grur1  10772  prlem934  10985  ltexprlem7  10994  supsr  11064  dedekind  11340  supadd  12154  supmullem2  12157  uzind  12659  iccsplit  13483  elfz0add  13625  predfz  13652  elfzoextl  13721  fsuppmapnn0fiub  13998  ccatval2  14585  swrdswrd  14712  pfxccatin12lem2a  14734  swrdccatin2  14736  pfxccatpfx2  14744  cshimadifsn0  14837  01sqrexlem6  15265  isercolllem2  15684  fsumcvg  15730  isumrpcl  15864  fprodcvg  15951  rpnnen2lem4  16240  fproddvdsd  16360  saddisj  16490  sadass  16496  bitsshft  16500  smuval2  16507  smupvallem  16508  smu01lem  16510  smueqlem  16515  reumodprminv  16831  ramub1lem1  17053  firest  17452  mrissmrid  17664  initoeu2lem0  18037  acsfiindd  18576  acsmapd  18577  dirge  18626  chndss  18639  issubmnd  18786  issubg2  19174  eqgid  19212  cyccom  19235  dprdff  20045  dprddisj2  20072  ablfac1c  20104  c0rnghm  20572  issubrng2  20595  subrgdvds  20623  issubrg2  20629  rnghmsscmap  20667  rngcsect  20673  funcrngcsetc  20677  rhmsscmap  20696  rhmsscrnghm  20702  ringcsect  20707  funcringcsetc  20711  rhmsubclem4  20725  lssssr  21009  lssats2  21055  lbspss  21137  lsmelval2  21140  lspprat  21211  lbsextlem2  21217  lbsextlem3  21218  rnglidlmmgm  21303  rnglidlmsgrp  21304  rnglidlrng  21305  lpigen  21393  psgndiflemB  21640  lsmcss  21732  obselocv  21768  f1lindf  21862  issubassa3  21906  mplcoe5lem  22080  mdetdiaglem  22646  cpmadugsumlemF  22924  toprntopon  22973  elcls  23121  clsndisj  23123  elcls3  23131  neindisj  23165  lpval  23187  lpsscls  23189  lpss3  23192  maxlp  23195  restntr  23230  ordtbas2  23239  ordtbas  23240  pnfnei  23268  mnfnei  23269  cncls2  23321  lmcnp  23352  lpcls  23412  hauscmplem  23454  2ndcdisj  23504  kgen2ss  23603  txuni2  23613  ptpjpre1  23619  tx1cn  23657  tx2cn  23658  prdstopn  23676  txlm  23696  imasnopn  23738  imasncld  23739  imasncls  23740  tgqtop  23760  regr1lem  23787  fgss2  23922  uzfbas  23946  ufilmax  23955  uffix2  23972  ufildr  23979  fmfnfmlem1  24002  fmco  24009  flimrest  24031  fclsopn  24062  fclscf  24073  flimfcls  24074  alexsubALTlem4  24098  qustgplem  24169  imasf1oxms  24537  prdsbl  24539  metrest  24572  iccntr  24870  reconnlem2  24876  caucfil  25333  caussi  25347  bcthlem5  25378  ovoliunlem1  25552  shft2rab  25558  sca2rab  25562  ovolicc2  25572  vitalilem2  25659  vitalilem5  25662  mbfinf  25715  i1f1lem  25739  mbfi1fseqlem4  25768  itgss  25862  itgcn  25895  c1liplem1  26046  c1lip1  26047  c1lip3  26049  ply1remlem  26213  plyexmo  26365  taylply2  26419  lgamucov  27090  fsumvma  27265  logfaclbnd  27274  ltsres  27714  nosepssdm  27738  nodenselem8  27743  nosupno  27755  nosupbday  27757  noinfbday  27772  elmade  27938  oldssmade  27948  mulsproplem13  28209  mulsproplem14  28210  precsexlem10  28297  bdayons  28357  uzsind  28486  axlowdimlem16  29115  axcontlem9  29130  edgupgr  29292  upgredg  29295  subgreldmiedg  29441  upgrres1  29471  crctcshwlkn0lem2  29968  wwlksnred  30049  clwwlkccatlem  30148  clwwlkf  30206  wwlksubclwwlk  30217  eupth2lems  30397  sspmval  30893  sspimsval  30898  ubthlem1  31030  shsubcl  31380  shorth  31455  elspansn3  31732  elnlfn  32088  elpjrn  32350  sumdmdlem2  32579  nfpconfp  32795  xrofsup  32930  elrspunidl  33575  ressply1mon1p  33725  fldextrspunlsplem  33931  cmpcref  34108  zarclsiin  34129  cntmeas  34484  1stmbfm  34518  2ndmbfm  34519  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemodife  34756  ballotlemimin  34764  bnj1171  35256  bnj1280  35276  r1filimi  35360  subgrwlk  35443  gonarlem  35705  goalrlem  35707  mrsubrn  35824  elfzm12  35986  ontgval  36752  elttctr  36826  bj-restuni  37548  pibt2  37872  lindsenlbs  38075  poimirlem29  38109  poimirlem30  38110  poimirlem31  38111  itg2addnclem  38131  itg2addnclem2  38132  ftc1anclem7  38159  ismtyima  38263  suceldisj  39278  lshpkr  39702  psubatN  40340  elpaddn0  40385  pclfinN  40485  diael  41628  dia2dimlem12  41660  dicelval1stN  41773  dicelval2nd  41774  dib2dim  41828  dih2dimbALTN  41830  dihlspsnssN  41917  dvh1dim  42027  lcfrvalsnN  42126  mapdrvallem2  42230  mapdpglem2  42258  hdmap10lem  42424  hdmap11lem2  42427  hdmapoc  42516  primrootscoprbij  42680  primrootspoweq0  42684  aks6d1c2  42708  sticksstones3  42726  sticksstones17  42741  sticksstones18  42742  unitscyglem2  42774  unitscyglem4  42776  unitscyglem5  42777  isnacs3  43252  aomclem2  43593  kelac1  43601  rngunsnply  43707  safesnsupfiub  43953  intabssd  44056  iunrelexp0  44239  rfovcnvf1od  44541  rfovcnvfvd  44544  fsovrfovd  44546  clsk1indlem3  44580  neik0pk1imk0  44584  ntrneineine0lem  44620  ntrneiel2  44623  ntrneikb  44631  ntrneik4w  44637  mnuop3d  44808  dvconstbi  44871  expgrowth  44872  modelaxreplem2  45516  modelaxreplem3  45517  climsuselem1  46144  climsuse  46145  limcresiooub  46177  iblsplit  46501  iblspltprt  46508  stoweidlem62  46597  stirlinglem11  46619  fourierdlem41  46683  qndenserrnbllem  46829  sge0fodjrnlem  46951  smflimsuplem7  47361  fafvelcdm  47725  fafv2elcdm  47789  ceilhalfelfzo1  47889  smonoord  47932  muldvdsfacm1  47942  iccpartiltu  47989  iccpartigtl  47990  iccpartiun  48001  iccpartdisj  48004  bgoldbtbndlem2  48389  gpgedgvtx1  48645  lidldomn1  48814  rhmsubcALTVlem4  48867  funcringcsetcALTV2lem9  48881  lincresunit3lem1  49062  setrec1  50273  setis  50280  vsetrec  50285  pgindnf  50298