Theorem sseld 3853

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

Syntax hints:   → wi 4   ∈ wcel 2048   ⊆ wss 3825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-in 3832  df-ss 3839

This theorem is referenced by:  sselda  3854  sseldd  3855  ssneld  3856  elelpwi  4429  ssbrd  4966  uniopel  5255  exopxfr2  5558  dmrnssfld  5676  preddowncl  6007  opelf  6362  fvimacnv  6642  ffvelrn  6668  fnsnr  6744  f1imass  6841  onminex  7332  extmptsuppeq  7650  suppssr  7657  dftpos3  7706  wfrlem16  7767  oa00  7978  omordi  7985  omlimcl  7997  omeulem1  8001  nnmordi  8050  mapsnd  8240  ixpf  8273  pw2f1olem  8409  pssnn  8523  findcard3  8548  ixpfi2  8609  fissuni  8616  elfiun  8681  dffi3  8682  ordiso2  8766  ordtypelem7  8775  ixpiunwdom  8842  inf3lem2  8878  cantnfp1lem3  8929  cantnfp1  8930  cantnflem1  8938  cantnf  8942  trcl  8956  r1ordg  8993  rankelb  9039  rankuni2b  9068  rankval4  9082  tcrank  9099  cplem1  9104  carduniima  9308  alephfp  9320  kmlem2  9363  isf32lem3  9567  domtriomlem  9654  axdc3lem2  9663  zorn2lem7  9714  ttukeylem6  9726  iundom2g  9752  fpwwe2lem13  9854  tskss  9970  tskr1om2  9980  inatsk  9990  gruss  10008  gruel  10015  grur1  10032  prlem934  10245  ltexprlem7  10254  supsr  10324  dedekind  10595  supadd  11402  supmullem2  11405  uzind  11880  iccsplit  12680  elfz0add  12815  predfz  12841  fsuppmapnn0fiub  13167  ccatval2  13731  swrdswrd  13877  swrdccatin12lem2a  13916  swrdccatin2  13919  swrdccatin12lem2c  13920  pfxccatin12  13924  swrdccatin12OLD  13925  pfxccatpfx2  13931  cshimadifsn0  14044  sqrlem6  14458  isercolllem2  14873  fsumcvg  14919  isumrpcl  15048  fprodcvg  15134  rpnnen2lem4  15420  fproddvdsd  15534  saddisj  15664  sadass  15670  bitsshft  15674  smuval2  15681  smupvallem  15682  smu01lem  15684  smueqlem  15689  reumodprminv  15987  ramub1lem1  16208  firest  16552  mrissmrid  16760  initoeu2lem0  17121  acsfiindd  17635  acsmapd  17636  dirge  17695  issubmnd  17776  issubg2  18068  eqgid  18105  dprdff  18874  dprddisj2  18901  ablfac1c  18933  subrgdvds  19262  issubrg2  19268  lssssr  19437  lssats2  19484  lbspss  19566  lsmelval2  19569  lspprat  19637  lbsextlem2  19643  lbsextlem3  19644  lpigen  19740  mplcoe5lem  19951  psgndiflemB  20436  lsmcss  20528  obselocv  20564  f1lindf  20658  mdetdiaglem  20901  cpmadugsumlemF  21178  toprntopon  21227  elcls  21375  clsndisj  21377  elcls3  21385  neindisj  21419  lpval  21441  lpsscls  21443  lpss3  21446  maxlp  21449  restntr  21484  ordtbas2  21493  ordtbas  21494  pnfnei  21522  mnfnei  21523  cncls2  21575  lmcnp  21606  lpcls  21666  hauscmplem  21708  2ndcdisj  21758  kgen2ss  21857  txuni2  21867  ptpjpre1  21873  tx1cn  21911  tx2cn  21912  prdstopn  21930  txlm  21950  imasnopn  21992  imasncld  21993  imasncls  21994  tgqtop  22014  regr1lem  22041  fgss2  22176  uzfbas  22200  ufilmax  22209  uffix2  22226  ufildr  22233  fmfnfmlem1  22256  fmco  22263  flimrest  22285  fclsopn  22316  fclscf  22327  flimfcls  22328  alexsubALTlem4  22352  qustgplem  22422  imasf1oxms  22792  prdsbl  22794  metrest  22827  iccntr  23122  reconnlem2  23128  caucfil  23579  caussi  23593  bcthlem5  23624  ovoliunlem1  23796  shft2rab  23802  sca2rab  23806  ovolicc2  23816  vitalilem2  23903  vitalilem5  23906  mbfinf  23959  i1f1lem  23983  mbfi1fseqlem4  24012  itgss  24105  itgcn  24136  c1liplem1  24286  c1lip1  24287  c1lip3  24289  ply1remlem  24449  plyexmo  24595  lgamucov  25307  fsumvma  25481  logfaclbnd  25490  axlowdimlem16  26436  axcontlem9  26451  edgupgr  26612  upgredg  26615  subgreldmiedg  26758  upgrres1  26788  crctcshwlkn0lem2  27287  wwlksnred  27369  wwlksnredOLD  27370  wwlksnext  27371  clwwlkccatlem  27485  clwwlkfOLD  27554  clwwlkf  27559  wwlksubclwwlk  27571  wwlksubclwwlkOLD  27572  eupth2lems  27758  sspmval  28277  sspimsval  28282  sspphOLD  28399  ubthlem1  28415  shsubcl  28766  shorth  28843  elspansn3  29120  elnlfn  29476  elpjrn  29738  sumdmdlem2  29967  fimarab  30142  supssd  30186  infssd  30187  xrofsup  30233  cmpcref  30715  cntmeas  31087  1stmbfm  31120  2ndmbfm  31121  ballotlemfc0  31353  ballotlemfcc  31354  ballotlemodife  31358  ballotlemimin  31366  bnj1171  31878  bnj1280  31898  mrsubrn  32220  elfzm12  32378  trpredtr  32530  trpredmintr  32531  dftrpred3g  32533  trpredrec  32538  sltres  32630  nosepssdm  32651  nodenselem8  32656  nosupno  32664  nosupbday  32666  ontgval  33239  bj-restuni  33833  pibt2  34074  lindsenlbs  34276  poimirlem16  34297  poimirlem29  34310  poimirlem30  34311  poimirlem31  34312  itg2addnclem  34332  itg2addnclem2  34333  ftc1anclem7  34362  ismtyima  34471  lshpkr  35646  psubatN  36284  elpaddn0  36329  pclfinN  36429  diael  37572  dia2dimlem12  37604  dicelval1stN  37717  dicelval2nd  37718  dib2dim  37772  dih2dimbALTN  37774  dihlspsnssN  37861  dvh1dim  37971  lcfrvalsnN  38070  mapdrvallem2  38174  mapdpglem2  38202  hdmap10lem  38368  hdmap11lem2  38371  hdmapoc  38460  isnacs3  38647  aomclem2  38996  kelac1  39004  rngunsnply  39114  intabssd  39277  iunrelexp0  39355  rfovcnvf1od  39658  rfovcnvfvd  39661  fsovrfovd  39663  clsk1indlem3  39701  neik0pk1imk0  39705  ntrneineine0lem  39741  ntrneiel2  39744  ntrneikb  39752  ntrneik4w  39758  mnuop3d  39927  dvconstbi  40026  expgrowth  40027  climsuselem1  41265  climsuse  41266  limcresiooub  41300  iblsplit  41627  iblspltprt  41634  stoweidlem62  41724  stirlinglem11  41746  fourierdlem41  41810  qndenserrnbllem  41956  sge0fodjrnlem  42075  sssmf  42392  smflimsuplem7  42477  fafvelrn  42721  fafv2elrn  42785  smonoord  42883  iccpartiltu  42900  iccpartigtl  42901  iccpartiun  42912  iccpartdisj  42915  bgoldbtbndlem2  43279  c0rnghm  43488  lidldomn1  43496  lidlmmgm  43500  lidlmsgrp  43501  lidlrng  43502  rnghmsscmap  43549  rngcsect  43555  funcrngcsetc  43573  rhmsscmap  43595  rhmsscrnghm  43601  ringcsect  43606  funcringcsetc  43610  funcringcsetcALTV2lem9  43619  rhmsubclem4  43664  rhmsubcALTVlem4  43682  lincresunit3lem1  43841  setrec1  44101  setis  44107  vsetrec  44112