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 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2840  df-ss 3923

This theorem is used by:  sselda  3938  sseldd  3939  ssneld  3940  eqrrabd  4041  elelpwi  4574  ssbrd  5156  uniopel  5501  exopxfr2  5832  dmrnssfld  5966  preddowncl  6337  opelf  6743  elfvunirn  6915  fimarab  6959  fvimacnv  7052  ffvelcdm  7080  fnsnr  7165  f1imass  7264  onminex  7803  xpord2pred  8143  extmptsuppeq  8186  suppssr  8193  suppssrg  8194  dftpos3  8242  oa00  8546  omordi  8553  omlimcl  8565  omeulem1  8569  nnmordi  8619  mapsnd  8886  ixpf  8920  pw2f1olem  9072  pssnn  9156  findcard3  9246  ixpfi2  9310  fissuni  9317  elfiun  9393  dffi3  9394  supssd  9426  infssd  9457  ordiso2  9480  ordtypelem7  9489  ixpiunwdom  9555  inf3lem2  9601  cantnfp1lem3  9652  cantnfp1  9653  cantnflem1  9661  cantnf  9665  trcl  9700  r1ordg  9753  rankelb  9799  rankuni2b  9828  rankval4  9842  tcrank  9859  cplem1  9882  cplem1OLD  9883  carduniima  10092  alephfp  10104  kmlem2  10147  isf32lem3  10350  domtriomlem  10437  axdc3lem2  10446  zorn2lem7  10497  ttukeylem6  10509  iundom2g  10535  fpwwe2lem12  10638  tskss  10754  tskr1om2  10764  inatsk  10774  gruss  10792  gruel  10799  grur1  10816  prlem934  11029  ltexprlem7  11038  supsr  11108  dedekind  11384  supadd  12194  supmullem2  12197  uzind  12700  iccsplit  13524  elfz0add  13667  predfz  13694  elfzoextl  13763  fsuppmapnn0fiub  14041  ccatval2  14629  swrdswrd  14760  pfxccatin12lem2a  14782  swrdccatin2  14784  pfxccatpfx2  14792  cshimadifsn0  14887  01sqrexlem6  15318  isercolllem2  15737  fsumcvg  15782  isumrpcl  15916  fprodcvg  16003  rpnnen2lem4  16291  fproddvdsd  16411  saddisj  16541  sadass  16547  bitsshft  16551  smuval2  16558  smupvallem  16559  smu01lem  16561  smueqlem  16566  reumodprminv  16882  ramub1lem1  17104  firest  17503  mrissmrid  17715  initoeu2lem0  18088  acsfiindd  18627  acsmapd  18628  dirge  18677  chndss  18690  issubmnd  18841  issubg2  19232  eqgid  19272  cyccom  19298  dprdff  20108  dprddisj2  20135  ablfac1c  20167  c0rnghm  20664  issubrng2  20687  subrgdvds  20715  issubrg2  20721  rnghmsscmap  20759  rngcsect  20765  funcrngcsetc  20769  rhmsscmap  20788  rhmsscrnghm  20794  ringcsect  20799  funcringcsetc  20803  rhmsubclem4  20817  lssssr  21105  lssats2  21151  lbspss  21233  lsmelval2  21236  lspprat  21307  lbsextlem2  21313  lbsextlem3  21314  rnglidlmmgm  21409  rnglidlmsgrp  21410  rnglidlrng  21411  df2idl2crng  21451  lpigen  21533  psgndiflemB  21780  lsmcss  21872  obselocv  21908  f1lindf  22002  issubassa3  22046  mplcoe5lem  22220  mdetdiaglem  22785  cpmadugsumlemF  23063  toprntopon  23112  elcls  23260  clsndisj  23262  elcls3  23270  neindisj  23304  lpval  23326  lpsscls  23328  lpss3  23331  maxlp  23334  restntr  23369  ordtbas2  23378  ordtbas  23379  pnfnei  23407  mnfnei  23408  cncls2  23460  lmcnp  23491  lpcls  23551  hauscmplem  23593  2ndcdisj  23644  kgen2ss  23743  txuni2  23753  ptpjpre1  23759  tx1cn  23797  tx2cn  23798  prdstopn  23816  txlm  23836  imasnopn  23878  imasncld  23879  imasncls  23880  tgqtop  23900  regr1lem  23927  fgss2  24062  uzfbas  24086  ufilmax  24095  uffix2  24112  ufildr  24119  fmfnfmlem1  24142  fmco  24149  flimrest  24171  fclsopn  24202  fclscf  24213  flimfcls  24214  alexsubALTlem4  24238  qustgplem  24309  imasf1oxms  24677  prdsbl  24679  metrest  24712  iccntr  25010  reconnlem2  25016  caucfil  25473  caussi  25487  bcthlem5  25518  ovoliunlem1  25692  shft2rab  25698  sca2rab  25702  ovolicc2  25712  vitalilem2  25799  vitalilem5  25802  mbfinf  25855  i1f1lem  25879  mbfi1fseqlem4  25908  itgss  26002  itgcn  26035  c1liplem1  26186  c1lip1  26187  c1lip3  26189  ply1remlem  26353  plyexmo  26505  taylply2  26562  lgamucov  27233  fsumvma  27408  logfaclbnd  27417  ltsres  27857  nosepssdm  27881  nodenselem8  27886  nosupno  27898  nosupbday  27900  noinfbday  27915  elmade  28081  oldssmade  28091  mulsproplem13  28352  mulsproplem14  28353  precsexlem10  28440  bdayons  28500  uzsind  28629  axlowdimlem16  29338  axcontlem9  29353  edgupgr  29515  upgredg  29518  subgreldmiedg  29667  upgrres1  29697  subgrwlk  30072  crctcshwlkn0lem2  30203  wwlksnred  30284  clwwlkccatlem  30383  clwwlkf  30441  wwlksubclwwlk  30452  eupth2lems  30636  sspmval  31132  sspimsval  31137  ubthlem1  31269  shsubcl  31619  shorth  31694  elspansn3  31971  elnlfn  32327  elpjrn  32589  sumdmdlem2  32818  nfpconfp  33024  xrofsup  33158  elrspunidl  33776  ressply1mon1p  33898  fldextrspunlsplem  34103  cmpcref  34280  zarclsiin  34301  cntmeas  34657  1stmbfm  34691  2ndmbfm  34692  ballotlemfc0  34924  ballotlemfcc  34925  ballotlemodife  34929  ballotlemimin  34937  bnj1171  35429  bnj1280  35449  r1filimi  35531  gonarlem  35899  goalrlem  35901  mrsubrn  36018  elfzm12  36180  ontgval  36975  elttctr  37049  bj-restuni  37772  pibt2  38096  lindsenlbs  38299  poimirlem29  38333  poimirlem30  38334  poimirlem31  38335  itg2addnclem  38355  itg2addnclem2  38356  ftc1anclem7  38383  ismtyima  38487  suceldisj  39500  lshpkr  39924  psubatN  40562  elpaddn0  40607  pclfinN  40707  diael  41850  dia2dimlem12  41882  dicelval1stN  41995  dicelval2nd  41996  dib2dim  42050  dih2dimbALTN  42052  dihlspsnssN  42139  dvh1dim  42249  lcfrvalsnN  42348  mapdrvallem2  42452  mapdpglem2  42480  hdmap10lem  42646  hdmap11lem2  42649  hdmapoc  42738  primrootscoprbij  42902  primrootspoweq0  42906  aks6d1c2  42930  sticksstones3  42948  sticksstones17  42963  sticksstones18  42964  unitscyglem2  42996  unitscyglem4  42998  unitscyglem5  42999  isnacs3  43474  aomclem2  43815  kelac1  43823  rngunsnply  43929  safesnsupfiub  44175  intabssd  44278  iunrelexp0  44461  rfovcnvf1od  44763  rfovcnvfvd  44766  fsovrfovd  44768  clsk1indlem3  44802  neik0pk1imk0  44806  ntrneineine0lem  44842  ntrneiel2  44845  ntrneikb  44853  ntrneik4w  44859  mnuop3d  45014  dvconstbi  45077  expgrowth  45078  modelaxreplem2  45721  modelaxreplem3  45722  climsuselem1  46356  climsuse  46357  limcresiooub  46389  iblsplit  46713  iblspltprt  46720  stoweidlem62  46809  stirlinglem11  46831  fourierdlem41  46895  qndenserrnbllem  47041  sge0fodjrnlem  47163  smflimsuplem7  47573  fafvelcdm  47940  fafv2elcdm  48004  ceilhalfelfzo1  48104  smonoord  48147  muldvdsfacm1  48157  iccpartiltu  48204  iccpartigtl  48205  iccpartiun  48216  iccpartdisj  48219  bgoldbtbndlem2  48604  gpgedgvtx1  48860  lidldomn1  49029  rhmsubcALTVlem4  49082  funcringcsetcALTV2lem9  49096  lincresunit3lem1  49292  setrec1  50502  setis  50509  vsetrec  50514  pgindnf  50527