Theorem sseld 3993

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-clel 2813  df-ss 3979

This theorem is referenced by:  sselda  3994  sseldd  3995  ssneld  3996  eqrrabd  4095  elelpwi  4614  ssbrd  5190  uniopel  5525  exopxfr2  5857  dmrnssfld  5986  preddowncl  6354  opelf  6769  elfvunirn  6938  fimarab  6982  fvimacnv  7072  ffvelcdm  7100  fnsnr  7184  f1imass  7283  onminex  7821  xpord2pred  8168  extmptsuppeq  8211  suppssr  8218  suppssrg  8219  dftpos3  8267  wfrlem16OLD  8362  oa00  8595  omordi  8602  omlimcl  8614  omeulem1  8618  nnmordi  8667  mapsnd  8924  ixpf  8958  pw2f1olem  9114  pssnn  9206  findcard3  9315  findcard3OLD  9316  ixpfi2  9387  fissuni  9394  elfiun  9467  dffi3  9468  ordiso2  9552  ordtypelem7  9561  ixpiunwdom  9627  inf3lem2  9666  cantnfp1lem3  9717  cantnfp1  9718  cantnflem1  9726  cantnf  9730  trcl  9765  r1ordg  9815  rankelb  9861  rankuni2b  9890  rankval4  9904  tcrank  9921  cplem1  9926  carduniima  10133  alephfp  10145  kmlem2  10189  isf32lem3  10392  domtriomlem  10479  axdc3lem2  10488  zorn2lem7  10539  ttukeylem6  10551  iundom2g  10577  fpwwe2lem12  10679  tskss  10795  tskr1om2  10805  inatsk  10815  gruss  10833  gruel  10840  grur1  10857  prlem934  11070  ltexprlem7  11079  supsr  11149  dedekind  11421  supadd  12233  supmullem2  12236  uzind  12707  iccsplit  13521  elfz0add  13662  predfz  13689  elfzoextl  13756  fsuppmapnn0fiub  14028  ccatval2  14612  swrdswrd  14739  pfxccatin12lem2a  14761  swrdccatin2  14763  pfxccatpfx2  14771  cshimadifsn0  14865  01sqrexlem6  15282  isercolllem2  15698  fsumcvg  15744  isumrpcl  15875  fprodcvg  15962  rpnnen2lem4  16249  fproddvdsd  16368  saddisj  16498  sadass  16504  bitsshft  16508  smuval2  16515  smupvallem  16516  smu01lem  16518  smueqlem  16523  reumodprminv  16837  ramub1lem1  17059  firest  17478  mrissmrid  17685  initoeu2lem0  18066  acsfiindd  18610  acsmapd  18611  dirge  18660  issubmnd  18786  issubg2  19171  eqgid  19210  cyccom  19233  dprdff  20046  dprddisj2  20073  ablfac1c  20105  c0rnghm  20551  issubrng2  20574  subrgdvds  20602  issubrg2  20608  rnghmsscmap  20646  rngcsect  20652  funcrngcsetc  20656  rhmsscmap  20675  rhmsscrnghm  20681  ringcsect  20686  funcringcsetc  20690  rhmsubclem4  20704  lssssr  20969  lssats2  21015  lbspss  21098  lsmelval2  21101  lspprat  21172  lbsextlem2  21178  lbsextlem3  21179  rnglidlmmgm  21272  rnglidlmsgrp  21273  rnglidlrng  21274  lpigen  21362  psgndiflemB  21635  lsmcss  21727  obselocv  21765  f1lindf  21859  issubassa3  21903  mplcoe5lem  22074  mdetdiaglem  22619  cpmadugsumlemF  22897  toprntopon  22946  elcls  23096  clsndisj  23098  elcls3  23106  neindisj  23140  lpval  23162  lpsscls  23164  lpss3  23167  maxlp  23170  restntr  23205  ordtbas2  23214  ordtbas  23215  pnfnei  23243  mnfnei  23244  cncls2  23296  lmcnp  23327  lpcls  23387  hauscmplem  23429  2ndcdisj  23479  kgen2ss  23578  txuni2  23588  ptpjpre1  23594  tx1cn  23632  tx2cn  23633  prdstopn  23651  txlm  23671  imasnopn  23713  imasncld  23714  imasncls  23715  tgqtop  23735  regr1lem  23762  fgss2  23897  uzfbas  23921  ufilmax  23930  uffix2  23947  ufildr  23954  fmfnfmlem1  23977  fmco  23984  flimrest  24006  fclsopn  24037  fclscf  24048  flimfcls  24049  alexsubALTlem4  24073  qustgplem  24144  imasf1oxms  24517  prdsbl  24519  metrest  24552  iccntr  24856  reconnlem2  24862  caucfil  25330  caussi  25344  bcthlem5  25375  ovoliunlem1  25550  shft2rab  25556  sca2rab  25560  ovolicc2  25570  vitalilem2  25657  vitalilem5  25660  mbfinf  25713  i1f1lem  25737  mbfi1fseqlem4  25767  itgss  25861  itgcn  25894  c1liplem1  26049  c1lip1  26050  c1lip3  26052  ply1remlem  26218  plyexmo  26369  taylply2  26423  lgamucov  27095  fsumvma  27271  logfaclbnd  27280  sltres  27721  nosepssdm  27745  nodenselem8  27750  nosupno  27762  nosupbday  27764  noinfbday  27779  elmade  27920  oldssmade  27930  mulsproplem13  28168  mulsproplem14  28169  precsexlem10  28254  uzsind  28405  axlowdimlem16  28986  axcontlem9  29001  edgupgr  29165  upgredg  29168  subgreldmiedg  29314  upgrres1  29344  crctcshwlkn0lem2  29840  wwlksnred  29921  clwwlkccatlem  30017  clwwlkf  30075  wwlksubclwwlk  30086  eupth2lems  30266  sspmval  30761  sspimsval  30766  ubthlem1  30898  shsubcl  31248  shorth  31323  elspansn3  31600  elnlfn  31956  elpjrn  32218  sumdmdlem2  32447  nfpconfp  32648  supssd  32726  infssd  32727  xrofsup  32777  elrspunidl  33435  ressply1mon1p  33572  cmpcref  33810  zarclsiin  33831  cntmeas  34206  1stmbfm  34241  2ndmbfm  34242  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemodife  34478  ballotlemimin  34486  bnj1171  34992  bnj1280  35012  subgrwlk  35116  gonarlem  35378  goalrlem  35380  mrsubrn  35497  elfzm12  35659  ontgval  36413  bj-restuni  37079  pibt2  37399  lindsenlbs  37601  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  itg2addnclem  37657  itg2addnclem2  37658  ftc1anclem7  37685  ismtyima  37789  lshpkr  39098  psubatN  39737  elpaddn0  39782  pclfinN  39882  diael  41025  dia2dimlem12  41057  dicelval1stN  41170  dicelval2nd  41171  dib2dim  41225  dih2dimbALTN  41227  dihlspsnssN  41314  dvh1dim  41424  lcfrvalsnN  41523  mapdrvallem2  41627  mapdpglem2  41655  hdmap10lem  41821  hdmap11lem2  41824  hdmapoc  41913  primrootscoprbij  42083  primrootspoweq0  42087  aks6d1c2  42111  sticksstones3  42129  sticksstones17  42144  sticksstones18  42145  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  isnacs3  42697  aomclem2  43043  kelac1  43051  rngunsnply  43157  safesnsupfiub  43405  intabssd  43508  iunrelexp0  43691  rfovcnvf1od  43993  rfovcnvfvd  43996  fsovrfovd  43998  clsk1indlem3  44032  neik0pk1imk0  44036  ntrneineine0lem  44072  ntrneiel2  44075  ntrneikb  44083  ntrneik4w  44089  mnuop3d  44266  dvconstbi  44329  expgrowth  44330  modelaxreplem2  44943  modelaxreplem3  44944  climsuselem1  45562  climsuse  45563  limcresiooub  45597  iblsplit  45921  iblspltprt  45928  stoweidlem62  46017  stirlinglem11  46039  fourierdlem41  46103  qndenserrnbllem  46249  sge0fodjrnlem  46371  smflimsuplem7  46781  fafvelcdm  47119  fafv2elcdm  47183  smonoord  47295  iccpartiltu  47346  iccpartigtl  47347  iccpartiun  47358  iccpartdisj  47361  bgoldbtbndlem2  47730  ceilhalfelfzo1  47950  gpgedgvtx1  47954  lidldomn1  48074  rhmsubcALTVlem4  48127  funcringcsetcALTV2lem9  48141  lincresunit3lem1  48324  setrec1  48921  setis  48928  vsetrec  48933  pgindnf  48946