Theorem sseld 3937

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-clel 2838  df-ss 3923

This theorem is referenced by:  sselda  3938  sseldd  3939  ssneld  3940  eqrrabd  4041  elelpwi  4573  ssbrd  5155  uniopel  5501  exopxfr2  5832  dmrnssfld  5966  preddowncl  6335  opelf  6741  elfvunirn  6913  fimarab  6957  fvimacnv  7050  ffvelcdm  7078  fnsnr  7163  f1imass  7264  onminex  7802  xpord2pred  8142  extmptsuppeq  8185  suppssr  8192  suppssrg  8193  dftpos3  8241  oa00  8545  omordi  8552  omlimcl  8564  omeulem1  8568  nnmordi  8618  mapsnd  8885  ixpf  8919  pw2f1olem  9070  pssnn  9154  findcard3  9244  ixpfi2  9308  fissuni  9315  elfiun  9391  dffi3  9392  supssd  9424  infssd  9455  ordiso2  9478  ordtypelem7  9487  ixpiunwdom  9553  inf3lem2  9599  cantnfp1lem3  9650  cantnfp1  9651  cantnflem1  9659  cantnf  9663  trcl  9698  r1ordg  9751  rankelb  9797  rankuni2b  9826  rankval4  9840  tcrank  9857  cplem1  9876  carduniima  10081  alephfp  10093  kmlem2  10136  isf32lem3  10340  domtriomlem  10427  axdc3lem2  10436  zorn2lem7  10487  ttukeylem6  10499  iundom2g  10525  fpwwe2lem12  10628  tskss  10744  tskr1om2  10754  inatsk  10764  gruss  10782  gruel  10789  grur1  10806  prlem934  11019  ltexprlem7  11028  supsr  11098  dedekind  11374  supadd  12184  supmullem2  12187  uzind  12689  iccsplit  13513  elfz0add  13656  predfz  13683  elfzoextl  13752  fsuppmapnn0fiub  14029  ccatval2  14617  swrdswrd  14744  pfxccatin12lem2a  14766  swrdccatin2  14768  pfxccatpfx2  14776  cshimadifsn0  14869  01sqrexlem6  15300  isercolllem2  15719  fsumcvg  15765  isumrpcl  15899  fprodcvg  15986  rpnnen2lem4  16274  fproddvdsd  16394  saddisj  16524  sadass  16530  bitsshft  16534  smuval2  16541  smupvallem  16542  smu01lem  16544  smueqlem  16549  reumodprminv  16865  ramub1lem1  17087  firest  17486  mrissmrid  17698  initoeu2lem0  18071  acsfiindd  18610  acsmapd  18611  dirge  18660  chndss  18673  issubmnd  18820  issubg2  19209  eqgid  19249  cyccom  19275  dprdff  20085  dprddisj2  20112  ablfac1c  20144  c0rnghm  20621  issubrng2  20644  subrgdvds  20672  issubrg2  20678  rnghmsscmap  20716  rngcsect  20722  funcrngcsetc  20726  rhmsscmap  20745  rhmsscrnghm  20751  ringcsect  20756  funcringcsetc  20760  rhmsubclem4  20774  lssssr  21056  lssats2  21102  lbspss  21184  lsmelval2  21187  lspprat  21258  lbsextlem2  21264  lbsextlem3  21265  rnglidlmmgm  21360  rnglidlmsgrp  21361  rnglidlrng  21362  df2idl2crng  21402  lpigen  21484  psgndiflemB  21731  lsmcss  21823  obselocv  21859  f1lindf  21953  issubassa3  21997  mplcoe5lem  22171  mdetdiaglem  22736  cpmadugsumlemF  23014  toprntopon  23063  elcls  23211  clsndisj  23213  elcls3  23221  neindisj  23255  lpval  23277  lpsscls  23279  lpss3  23282  maxlp  23285  restntr  23320  ordtbas2  23329  ordtbas  23330  pnfnei  23358  mnfnei  23359  cncls2  23411  lmcnp  23442  lpcls  23502  hauscmplem  23544  2ndcdisj  23594  kgen2ss  23693  txuni2  23703  ptpjpre1  23709  tx1cn  23747  tx2cn  23748  prdstopn  23766  txlm  23786  imasnopn  23828  imasncld  23829  imasncls  23830  tgqtop  23850  regr1lem  23877  fgss2  24012  uzfbas  24036  ufilmax  24045  uffix2  24062  ufildr  24069  fmfnfmlem1  24092  fmco  24099  flimrest  24121  fclsopn  24152  fclscf  24163  flimfcls  24164  alexsubALTlem4  24188  qustgplem  24259  imasf1oxms  24627  prdsbl  24629  metrest  24662  iccntr  24960  reconnlem2  24966  caucfil  25423  caussi  25437  bcthlem5  25468  ovoliunlem1  25642  shft2rab  25648  sca2rab  25652  ovolicc2  25662  vitalilem2  25749  vitalilem5  25752  mbfinf  25805  i1f1lem  25829  mbfi1fseqlem4  25858  itgss  25952  itgcn  25985  c1liplem1  26136  c1lip1  26137  c1lip3  26139  ply1remlem  26303  plyexmo  26455  taylply2  26512  lgamucov  27183  fsumvma  27358  logfaclbnd  27367  ltsres  27807  nosepssdm  27831  nodenselem8  27836  nosupno  27848  nosupbday  27850  noinfbday  27865  elmade  28031  oldssmade  28041  mulsproplem13  28302  mulsproplem14  28303  precsexlem10  28390  bdayons  28450  uzsind  28579  axlowdimlem16  29288  axcontlem9  29303  edgupgr  29465  upgredg  29468  subgreldmiedg  29614  upgrres1  29644  crctcshwlkn0lem2  30141  wwlksnred  30222  clwwlkccatlem  30321  clwwlkf  30379  wwlksubclwwlk  30390  eupth2lems  30570  sspmval  31066  sspimsval  31071  ubthlem1  31203  shsubcl  31553  shorth  31628  elspansn3  31905  elnlfn  32261  elpjrn  32523  sumdmdlem2  32752  nfpconfp  32958  xrofsup  33093  elrspunidl  33717  ressply1mon1p  33839  fldextrspunlsplem  34044  cmpcref  34221  zarclsiin  34242  cntmeas  34597  1stmbfm  34631  2ndmbfm  34632  ballotlemfc0  34864  ballotlemfcc  34865  ballotlemodife  34869  ballotlemimin  34877  bnj1171  35369  bnj1280  35389  r1filimi  35478  subgrwlk  35605  gonarlem  35867  goalrlem  35869  mrsubrn  35986  elfzm12  36148  ontgval  36923  elttctr  36997  bj-restuni  37720  pibt2  38044  lindsenlbs  38247  poimirlem29  38281  poimirlem30  38282  poimirlem31  38283  itg2addnclem  38303  itg2addnclem2  38304  ftc1anclem7  38331  ismtyima  38435  suceldisj  39448  lshpkr  39872  psubatN  40510  elpaddn0  40555  pclfinN  40655  diael  41798  dia2dimlem12  41830  dicelval1stN  41943  dicelval2nd  41944  dib2dim  41998  dih2dimbALTN  42000  dihlspsnssN  42087  dvh1dim  42197  lcfrvalsnN  42296  mapdrvallem2  42400  mapdpglem2  42428  hdmap10lem  42594  hdmap11lem2  42597  hdmapoc  42686  primrootscoprbij  42850  primrootspoweq0  42854  aks6d1c2  42878  sticksstones3  42896  sticksstones17  42911  sticksstones18  42912  unitscyglem2  42944  unitscyglem4  42946  unitscyglem5  42947  isnacs3  43424  aomclem2  43765  kelac1  43773  rngunsnply  43879  safesnsupfiub  44125  intabssd  44228  iunrelexp0  44411  rfovcnvf1od  44713  rfovcnvfvd  44716  fsovrfovd  44718  clsk1indlem3  44752  neik0pk1imk0  44756  ntrneineine0lem  44792  ntrneiel2  44795  ntrneikb  44803  ntrneik4w  44809  mnuop3d  44964  dvconstbi  45027  expgrowth  45028  modelaxreplem2  45671  modelaxreplem3  45672  climsuselem1  46306  climsuse  46307  limcresiooub  46339  iblsplit  46663  iblspltprt  46670  stoweidlem62  46759  stirlinglem11  46781  fourierdlem41  46845  qndenserrnbllem  46991  sge0fodjrnlem  47113  smflimsuplem7  47523  fafvelcdm  47890  fafv2elcdm  47954  ceilhalfelfzo1  48054  smonoord  48097  muldvdsfacm1  48107  iccpartiltu  48154  iccpartigtl  48155  iccpartiun  48166  iccpartdisj  48169  bgoldbtbndlem2  48554  gpgedgvtx1  48810  lidldomn1  48979  rhmsubcALTVlem4  49032  funcringcsetcALTV2lem9  49046  lincresunit3lem1  49242  setrec1  50452  setis  50459  vsetrec  50464  pgindnf  50477