Theorem sseld 3920

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-clel 2811  df-ss 3906

This theorem is referenced by:  sselda  3921  sseldd  3922  ssneld  3923  eqrrabd  4026  elelpwi  4551  ssbrd  5128  uniopel  5470  exopxfr2  5799  dmrnssfld  5929  preddowncl  6296  opelf  6701  elfvunirn  6870  fimarab  6914  fvimacnv  7005  ffvelcdm  7033  fnsnr  7118  f1imass  7219  onminex  7756  xpord2pred  8095  extmptsuppeq  8138  suppssr  8145  suppssrg  8146  dftpos3  8194  oa00  8494  omordi  8501  omlimcl  8513  omeulem1  8517  nnmordi  8567  mapsnd  8834  ixpf  8868  pw2f1olem  9019  pssnn  9103  findcard3  9193  ixpfi2  9260  fissuni  9267  elfiun  9343  dffi3  9344  supssd  9376  infssd  9407  ordiso2  9430  ordtypelem7  9439  ixpiunwdom  9505  inf3lem2  9550  cantnfp1lem3  9601  cantnfp1  9602  cantnflem1  9610  cantnf  9614  trcl  9649  r1ordg  9702  rankelb  9748  rankuni2b  9777  rankval4  9791  tcrank  9808  cplem1  9813  carduniima  10018  alephfp  10030  kmlem2  10074  isf32lem3  10277  domtriomlem  10364  axdc3lem2  10373  zorn2lem7  10424  ttukeylem6  10436  iundom2g  10462  fpwwe2lem12  10565  tskss  10681  tskr1om2  10691  inatsk  10701  gruss  10719  gruel  10726  grur1  10743  prlem934  10956  ltexprlem7  10965  supsr  11035  dedekind  11309  supadd  12124  supmullem2  12127  uzind  12621  iccsplit  13438  elfz0add  13580  predfz  13607  elfzoextl  13676  fsuppmapnn0fiub  13953  ccatval2  14540  swrdswrd  14667  pfxccatin12lem2a  14689  swrdccatin2  14691  pfxccatpfx2  14699  cshimadifsn0  14792  01sqrexlem6  15209  isercolllem2  15628  fsumcvg  15674  isumrpcl  15808  fprodcvg  15895  rpnnen2lem4  16184  fproddvdsd  16304  saddisj  16434  sadass  16440  bitsshft  16444  smuval2  16451  smupvallem  16452  smu01lem  16454  smueqlem  16459  reumodprminv  16775  ramub1lem1  16997  firest  17395  mrissmrid  17607  initoeu2lem0  17980  acsfiindd  18519  acsmapd  18520  dirge  18569  chndss  18582  issubmnd  18729  issubg2  19117  eqgid  19155  cyccom  19178  dprdff  19989  dprddisj2  20016  ablfac1c  20048  c0rnghm  20512  issubrng2  20535  subrgdvds  20563  issubrg2  20569  rnghmsscmap  20607  rngcsect  20613  funcrngcsetc  20617  rhmsscmap  20636  rhmsscrnghm  20642  ringcsect  20647  funcringcsetc  20651  rhmsubclem4  20665  lssssr  20949  lssats2  20995  lbspss  21077  lsmelval2  21080  lspprat  21151  lbsextlem2  21157  lbsextlem3  21158  rnglidlmmgm  21243  rnglidlmsgrp  21244  rnglidlrng  21245  lpigen  21333  psgndiflemB  21580  lsmcss  21672  obselocv  21708  f1lindf  21802  issubassa3  21846  mplcoe5lem  22017  mdetdiaglem  22563  cpmadugsumlemF  22841  toprntopon  22890  elcls  23038  clsndisj  23040  elcls3  23048  neindisj  23082  lpval  23104  lpsscls  23106  lpss3  23109  maxlp  23112  restntr  23147  ordtbas2  23156  ordtbas  23157  pnfnei  23185  mnfnei  23186  cncls2  23238  lmcnp  23269  lpcls  23329  hauscmplem  23371  2ndcdisj  23421  kgen2ss  23520  txuni2  23530  ptpjpre1  23536  tx1cn  23574  tx2cn  23575  prdstopn  23593  txlm  23613  imasnopn  23655  imasncld  23656  imasncls  23657  tgqtop  23677  regr1lem  23704  fgss2  23839  uzfbas  23863  ufilmax  23872  uffix2  23889  ufildr  23896  fmfnfmlem1  23919  fmco  23926  flimrest  23948  fclsopn  23979  fclscf  23990  flimfcls  23991  alexsubALTlem4  24015  qustgplem  24086  imasf1oxms  24454  prdsbl  24456  metrest  24489  iccntr  24787  reconnlem2  24793  caucfil  25250  caussi  25264  bcthlem5  25295  ovoliunlem1  25469  shft2rab  25475  sca2rab  25479  ovolicc2  25489  vitalilem2  25576  vitalilem5  25579  mbfinf  25632  i1f1lem  25656  mbfi1fseqlem4  25685  itgss  25779  itgcn  25812  c1liplem1  25963  c1lip1  25964  c1lip3  25966  ply1remlem  26130  plyexmo  26279  taylply2  26333  lgamucov  27001  fsumvma  27176  logfaclbnd  27185  ltsres  27626  nosepssdm  27650  nodenselem8  27655  nosupno  27667  nosupbday  27669  noinfbday  27684  elmade  27849  oldssmade  27859  mulsproplem13  28120  mulsproplem14  28121  precsexlem10  28208  bdayons  28268  uzsind  28397  axlowdimlem16  29026  axcontlem9  29041  edgupgr  29203  upgredg  29206  subgreldmiedg  29352  upgrres1  29382  crctcshwlkn0lem2  29879  wwlksnred  29960  clwwlkccatlem  30059  clwwlkf  30117  wwlksubclwwlk  30128  eupth2lems  30308  sspmval  30804  sspimsval  30809  ubthlem1  30941  shsubcl  31291  shorth  31366  elspansn3  31643  elnlfn  31999  elpjrn  32261  sumdmdlem2  32490  nfpconfp  32705  xrofsup  32840  elrspunidl  33488  ressply1mon1p  33628  fldextrspunlsplem  33817  cmpcref  33994  zarclsiin  34015  cntmeas  34370  1stmbfm  34404  2ndmbfm  34405  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemodife  34642  ballotlemimin  34650  bnj1171  35142  bnj1280  35162  r1filimi  35246  subgrwlk  35314  gonarlem  35576  goalrlem  35578  mrsubrn  35695  elfzm12  35857  ontgval  36613  elttctr  36687  bj-restuni  37409  pibt2  37733  lindsenlbs  37936  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  itg2addnclem  37992  itg2addnclem2  37993  ftc1anclem7  38020  ismtyima  38124  suceldisj  39139  lshpkr  39563  psubatN  40201  elpaddn0  40246  pclfinN  40346  diael  41489  dia2dimlem12  41521  dicelval1stN  41634  dicelval2nd  41635  dib2dim  41689  dih2dimbALTN  41691  dihlspsnssN  41778  dvh1dim  41888  lcfrvalsnN  41987  mapdrvallem2  42091  mapdpglem2  42119  hdmap10lem  42285  hdmap11lem2  42288  hdmapoc  42377  primrootscoprbij  42541  primrootspoweq0  42545  aks6d1c2  42569  sticksstones3  42587  sticksstones17  42602  sticksstones18  42603  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  isnacs3  43142  aomclem2  43483  kelac1  43491  rngunsnply  43597  safesnsupfiub  43843  intabssd  43946  iunrelexp0  44129  rfovcnvf1od  44431  rfovcnvfvd  44434  fsovrfovd  44436  clsk1indlem3  44470  neik0pk1imk0  44474  ntrneineine0lem  44510  ntrneiel2  44513  ntrneikb  44521  ntrneik4w  44527  mnuop3d  44698  dvconstbi  44761  expgrowth  44762  modelaxreplem2  45406  modelaxreplem3  45407  climsuselem1  46037  climsuse  46038  limcresiooub  46070  iblsplit  46394  iblspltprt  46401  stoweidlem62  46490  stirlinglem11  46512  fourierdlem41  46576  qndenserrnbllem  46722  sge0fodjrnlem  46844  smflimsuplem7  47254  fafvelcdm  47618  fafv2elcdm  47682  ceilhalfelfzo1  47782  smonoord  47825  muldvdsfacm1  47835  iccpartiltu  47882  iccpartigtl  47883  iccpartiun  47894  iccpartdisj  47897  bgoldbtbndlem2  48282  gpgedgvtx1  48538  lidldomn1  48707  rhmsubcALTVlem4  48760  funcringcsetcALTV2lem9  48774  lincresunit3lem1  48955  setrec1  50166  setis  50173  vsetrec  50178  pgindnf  50191