Theorem sseld 3908

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-clel 2835  df-ss 3897

This theorem is used by:  sselda  3909  sseldd  3910  ssneld  3911  eqrrabd  4010  elelpwi  4566  ssbrd  5147  uniopel  5488  exopxfr2  5822  dmrnssfld  5956  preddowncl  6337  opelf  6746  elfvunirn  6918  fimarab  6962  fvimacnv  7055  ffvelcdm  7084  fnsnr  7171  f1imass  7270  onminex  7818  xpord2pred  8166  extmptsuppeq  8210  suppssr  8217  suppssrg  8218  dftpos3  8266  oa00  8572  omordi  8579  omlimcl  8591  omeulem1  8595  nnmordi  8645  mapsnd  8919  ixpf  8953  pw2f1olem  9105  pssnn  9189  findcard3  9279  ixpfi2  9344  fissuni  9351  elfiun  9427  dffi3  9428  supssd  9460  infssd  9491  ordiso2  9514  ordtypelem7  9523  ixpiunwdom  9589  inf3lem2  9635  cantnfp1lem3  9686  cantnfp1  9687  cantnflem1  9695  cantnf  9699  trcl  9734  r1ordg  9790  rankelb  9838  rankuni2b  9872  rankval4  9889  tcrank  9906  r1filimi  9908  cplem1  9955  cplem1OLD  9956  setrec1  9977  carduniima  10180  alephfp  10192  kmlem2  10235  isf32lem3  10438  domtriomlem  10525  axdc3lem2  10534  zorn2lem7  10585  ttukeylem6  10597  iundom2g  10629  fpwwe2lem12  10732  tskss  10848  tskhf  10858  inatsk  10868  gruss  10886  gruel  10893  grur1  10910  prlem934  11123  ltexprlem7  11132  supsr  11202  dedekind  11478  supadd  12290  supmullem2  12293  uzind  12796  iccsplit  13621  elfz0add  13765  predfz  13792  elfzoextl  13861  fsuppmapnn0fiub  14139  ccatval2  14728  swrdswrd  14860  pfxccatin12lem2a  14882  swrdccatin2  14884  pfxccatpfx2  14892  cshimadifsn0  14987  01sqrexlem6  15421  isercolllem2  15840  fsumcvg  15885  isumrpcl  16019  fprodcvg  16104  rpnnen2lem4  16392  fproddvdsd  16512  saddisj  16642  sadass  16648  bitsshft  16652  smuval2  16659  smupvallem  16660  smu01lem  16662  smueqlem  16667  reumodprminv  16989  ramub1lem1  17211  firest  17610  mrissmrid  17822  initoeu2lem0  18195  acsfiindd  18734  acsmapd  18735  dirge  18784  chndss  18797  issubmnd  18960  issubg2  19359  eqgid  19399  cyccom  19425  dprdff  20235  dprddisj2  20262  ablfac1c  20294  c0rnghm  20794  issubrng2  20817  subrgdvds  20845  issubrg2  20851  rnghmsscmap  20889  rngcsect  20895  funcrngcsetc  20899  rhmsscmap  20918  rhmsscrnghm  20924  ringcsect  20929  funcringcsetc  20933  rhmsubclem4  20947  lssssr  21236  lssats2  21282  lbspss  21364  lsmelval2  21367  lspprat  21438  lbsextlem2  21444  lbsextlem3  21445  rnglidlmmgm  21540  rnglidlmsgrp  21541  rnglidlrng  21542  df2idl2crng  21584  lpigen  21666  psgndiflemB  21913  lsmcss  22005  obselocv  22041  f1lindf  22135  lindsenlbs  22164  issubassa3  22181  mplcoe5lem  22355  mdetdiaglem  22920  cpmadugsumlemF  23201  toprntopon  23250  elcls  23398  clsndisj  23400  elcls3  23408  neindisj  23442  lpval  23464  lpsscls  23466  lpss3  23469  maxlp  23472  restntr  23507  ordtbas2  23516  ordtbas  23517  pnfnei  23545  mnfnei  23546  cncls2  23598  lmcnp  23629  lpcls  23689  hauscmplem  23731  2ndcdisj  23782  kgen2ss  23881  txuni2  23891  ptpjpre1  23897  tx1cn  23935  tx2cn  23936  prdstopn  23954  txlm  23974  imasnopn  24016  imasncld  24017  imasncls  24018  tgqtop  24038  regr1lem  24065  fgss2  24200  uzfbas  24224  ufilmax  24233  uffix2  24250  ufildr  24257  fmfnfmlem1  24280  fmco  24287  flimrest  24309  fclsopn  24340  fclscf  24351  flimfcls  24352  alexsubALTlem4  24376  qustgplem  24447  imasf1oxms  24815  prdsbl  24817  metrest  24850  iccntr  25148  reconnlem2  25154  caucfil  25611  caussi  25625  bcthlem5  25656  ovoliunlem1  25830  shft2rab  25836  sca2rab  25840  ovolicc2  25850  vitalilem2  25937  vitalilem5  25940  mbfinf  25993  i1f1lem  26017  mbfi1fseqlem4  26046  itgss  26139  itgcn  26172  c1liplem1  26323  c1lip1  26324  c1lip3  26326  ply1remlem  26490  plyconz  26638  plyexmo  26643  taylply2  26702  lgamucov  27372  fsumvma  27547  logfaclbnd  27556  ltsres  28026  nosepssdm  28050  nodenselem8  28055  nosupno  28067  nosupbday  28069  noinfbday  28084  elmade  28250  oldssmade  28260  mulsproplem13  28521  mulsproplem14  28522  precsexlem10  28609  bdayons  28669  uzsind  28798  axlowdimlem16  29542  axcontlem9  29557  edgupgr  29719  upgredg  29722  subgreldmiedg  29871  upgrres1  29901  subgrwlk  30276  crctcshwlkn0lem2  30407  wwlksnred  30488  clwwlkccatlem  30587  clwwlkf  30645  wwlksubclwwlk  30656  eupth2lems  30846  sspmval  31342  sspimsval  31347  ubthlem1  31479  shsubcl  31829  shorth  31904  elspansn3  32181  elnlfn  32537  elpjrn  32799  sumdmdlem2  33028  nfpconfp  33275  xrofsup  33407  elrspunidl  34026  ressply1mon1p  34148  fldextrspunlsplem  34353  cmpcref  34530  zarclsiin  34551  cntmeas  34907  1stmbfm  34940  2ndmbfm  34941  ballotlemfc0  35173  ballotlemfcc  35174  ballotlemodife  35178  ballotlemimin  35186  bnj1171  35678  bnj1280  35698  ptpconn  36086  gonarlem  36247  goalrlem  36249  mrsubrn  36366  elfzm12  36528  ontgval  37313  elttctr  37387  bj-restuni  38124  pibt2  38447  poimirlem29  38674  poimirlem30  38675  poimirlem31  38676  itg2addnclem  38696  itg2addnclem2  38697  ftc1anclem7  38724  ismtyima  38844  suceldisj  39857  lshpkr  40281  psubatN  40919  elpaddn0  40964  pclfinN  41064  diael  42207  dia2dimlem12  42239  dicelval1stN  42352  dicelval2nd  42353  dib2dim  42407  dih2dimbALTN  42409  dihlspsnssN  42496  dvh1dim  42606  lcfrvalsnN  42705  mapdrvallem2  42809  mapdpglem2  42837  hdmap10lem  43003  hdmap11lem2  43006  hdmapoc  43095  primrootscoprbij  43259  primrootspoweq0  43263  aks6d1c2  43287  sticksstones3  43305  sticksstones17  43320  sticksstones18  43321  unitscyglem2  43353  unitscyglem4  43355  unitscyglem5  43356  isnacs3  43828  aomclem2  44164  kelac1  44172  rngunsnply  44278  safesnsupfiub  44524  intabssd  44627  iunrelexp0  44809  rfovcnvf1od  45111  rfovcnvfvd  45114  fsovrfovd  45116  clsk1indlem3  45150  neik0pk1imk0  45154  ntrneineine0lem  45190  ntrneiel2  45193  ntrneikb  45201  ntrneik4w  45207  mnuop3d  45362  dvconstbi  45425  expgrowth  45426  cocanss2  46029  modelaxreplem2  46076  modelaxreplem3  46077  climsuselem1  46726  climsuse  46727  limcresiooub  46759  iblsplit  47083  iblspltprt  47090  stoweidlem62  47179  stirlinglem11  47201  fourierdlem41  47265  qndenserrnbllem  47411  sge0fodjrnlem  47533  smflimsuplem7  47943  fafvelcdm  48347  fafv2elcdm  48411  ceilhalfelfzo1  48511  smonoord  48554  muldvdsfacm1  48564  iccpartiltu  48611  iccpartigtl  48612  iccpartiun  48623  iccpartdisj  48626  bgoldbtbndlem2  49011  gpgedgvtx1  49267  lidldomn1  49435  rhmsubcALTVlem4  49488  funcringcsetcALTV2lem9  49502  lincresunit3lem1  49698  setis  50973  vsetrec  50978  pgindnf  50991