Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseld Structured version   Visualization version   GIF version

Theorem sseld 3635
 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
StepHypRef Expression
1 sseld.1 . 2 (𝜑𝐴𝐵)
2 ssel 3630 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2030   ⊆ wss 3607 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621 This theorem is referenced by:  sselda  3636  sseldd  3637  ssneld  3638  elelpwi  4204  ssbrd  4728  uniopel  5007  exopxfr2  5299  dmrnssfld  5416  preddowncl  5745  nfunv  5959  opelf  6103  fvimacnv  6372  ffvelrn  6397  fnsnr  6472  f1imass  6561  onminex  7049  extmptsuppeq  7364  suppssr  7371  dftpos3  7415  wfrlem16  7475  oa00  7684  omordi  7691  omlimcl  7703  omeulem1  7707  nnmordi  7756  mapsn  7941  ixpf  7972  pw2f1olem  8105  pssnn  8219  findcard3  8244  ixpfi2  8305  fissuni  8312  elfiun  8377  dffi3  8378  ordiso2  8461  ordtypelem7  8470  ixpiunwdom  8537  inf3lem2  8564  cantnfp1lem3  8615  cantnfp1  8616  cantnflem1  8624  cantnf  8628  trcl  8642  r1ordg  8679  rankelb  8725  rankuni2b  8754  rankval4  8768  tcrank  8785  cplem1  8790  carduniima  8957  alephfp  8969  kmlem2  9011  isf32lem3  9215  domtriomlem  9302  axdc3lem2  9311  ac6num  9339  zorn2lem7  9362  ttukeylem6  9374  iundom2g  9400  fpwwe2lem13  9502  tskss  9618  tskr1om2  9628  inatsk  9638  gruss  9656  gruel  9663  grur1  9680  prlem934  9893  ltexprlem7  9902  supsr  9971  dedekind  10238  supadd  11029  supmullem2  11032  uzind  11507  iccsplit  12343  elfz0add  12477  predfz  12503  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  ccatval2  13396  swrdswrd  13506  swrdccatin12lem2a  13531  swrdccatin2  13533  swrdccatin12lem2c  13534  swrdccatin12  13537  cshimadifsn0  13622  sqrlem6  14032  isercolllem2  14440  fsumcvg  14487  isumrpcl  14619  fprodcvg  14704  rpnnen2lem4  14990  fproddvdsd  15106  saddisj  15234  sadass  15240  bitsshft  15244  smuval2  15251  smupvallem  15252  smu01lem  15254  smueqlem  15259  reumodprminv  15556  ramub1lem1  15777  firest  16140  mrissmrid  16348  initoeu2lem0  16710  acsfiindd  17224  acsmapd  17225  dirge  17284  issubmnd  17365  issubg2  17656  eqgid  17693  dprdff  18457  dprddisj2  18484  ablfac1c  18516  subrgdvds  18842  issubrg2  18848  lssssr  19001  lssats2  19048  lbspss  19130  lsmelval2  19133  lspprat  19201  lbsextlem2  19207  lbsextlem3  19208  lpigen  19304  mplcoe5lem  19515  psgndiflemB  19994  lsmcss  20084  obselocv  20120  f1lindf  20209  mdetdiaglem  20452  cpmadugsumlemF  20729  toprntopon  20777  elcls  20925  clsndisj  20927  elcls3  20935  neindisj  20969  lpval  20991  lpsscls  20993  lpss3  20996  maxlp  20999  restntr  21034  ordtbas2  21043  ordtbas  21044  pnfnei  21072  mnfnei  21073  cncls2  21125  lmcnp  21156  lpcls  21216  hauscmplem  21257  2ndcdisj  21307  kgen2ss  21406  txuni2  21416  ptpjpre1  21422  tx1cn  21460  tx2cn  21461  prdstopn  21479  txlm  21499  imasnopn  21541  imasncld  21542  imasncls  21543  tgqtop  21563  regr1lem  21590  fgss2  21725  uzfbas  21749  ufilmax  21758  uffix2  21775  ufildr  21782  fmfnfmlem1  21805  fmco  21812  flimrest  21834  fclsopn  21865  fclscf  21876  flimfcls  21877  alexsubALTlem4  21901  qustgplem  21971  imasf1oxms  22341  prdsbl  22343  metrest  22376  iccntr  22671  reconnlem2  22677  caucfil  23127  caussi  23141  bcthlem5  23171  ovoliunlem1  23316  shft2rab  23322  sca2rab  23326  ovolicc2  23336  vitalilem2  23423  vitalilem5  23426  mbfinf  23477  i1f1lem  23501  mbfi1fseqlem4  23530  itgss  23623  itgcn  23654  c1liplem1  23804  c1lip1  23805  c1lip3  23807  ply1remlem  23967  plyexmo  24113  lgamucov  24809  fsumvma  24983  logfaclbnd  24992  axlowdimlem16  25882  axcontlem9  25897  edgupgr  26074  upgredg  26077  subgreldmiedg  26220  upgrres1  26250  crctcshwlkn0lem2  26759  wwlksnred  26855  wwlksnext  26856  clwwlkf  27010  wwlksubclwwlk  27023  eupth2lems  27216  clwwlkccatlem  27331  sspmval  27716  sspimsval  27721  sspph  27838  ubthlem1  27854  shsubcl  28205  shorth  28282  elspansn3  28559  elnlfn  28915  elpjrn  29177  sumdmdlem2  29406  fimarab  29573  supssd  29615  infssd  29616  xrofsup  29661  cmpcref  30045  cntmeas  30417  1stmbfm  30450  2ndmbfm  30451  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemodife  30687  ballotlemimin  30695  bnj1171  31194  bnj1280  31214  mrsubrn  31536  elfzm12  31695  trpredtr  31854  trpredmintr  31855  dftrpred3g  31857  trpredrec  31862  sltres  31940  nosepssdm  31961  nodenselem8  31966  nosupno  31974  nosupbday  31976  ontgval  32555  bj-restuni  33175  lindsenlbs  33534  poimirlem16  33555  poimirlem29  33568  poimirlem30  33569  poimirlem31  33570  itg2addnclem  33591  itg2addnclem2  33592  ftc1anclem7  33621  ismtyima  33732  lshpkr  34722  psubatN  35359  elpaddn0  35404  pclfinN  35504  diael  36649  dia2dimlem12  36681  dicelval1stN  36794  dicelval2nd  36795  dib2dim  36849  dih2dimbALTN  36851  dihlspsnssN  36938  dvh1dim  37048  lcfrvalsnN  37147  mapdrvallem2  37251  mapdpglem2  37279  hdmap10lem  37448  hdmap11lem2  37451  hdmapoc  37540  isnacs3  37590  aomclem2  37942  kelac1  37950  rngunsnply  38060  intabssd  38233  iunrelexp0  38311  rfovcnvf1od  38615  rfovcnvfvd  38618  fsovrfovd  38620  clsk1indlem3  38658  neik0pk1imk0  38662  ntrneineine0lem  38698  ntrneiel2  38701  ntrneikb  38709  ntrneik4w  38715  dvconstbi  38850  expgrowth  38851  mapsnd  39702  climsuselem1  40157  climsuse  40158  limcresiooub  40192  iblsplit  40500  iblspltprt  40507  stoweidlem62  40597  stirlinglem11  40619  fourierdlem41  40683  qndenserrnbllem  40832  sge0fodjrnlem  40951  sssmf  41268  smflimsuplem7  41353  fafvelrn  41571  smonoord  41666  iccpartiltu  41683  iccpartigtl  41684  iccpartiun  41695  iccpartdisj  41698  pfxccatin12  41750  pfxccatpfx2  41753  bgoldbtbndlem2  42019  c0rnghm  42238  lidldomn1  42246  lidlmmgm  42250  lidlmsgrp  42251  lidlrng  42252  rnghmsscmap  42299  rngcsect  42305  funcrngcsetc  42323  rhmsscmap  42345  rhmsscrnghm  42351  ringcsect  42356  funcringcsetc  42360  funcringcsetcALTV2lem9  42369  rhmsubclem4  42414  rhmsubcALTVlem4  42432  lincresunit3lem1  42593  setrec1  42763  setis  42769  vsetrec  42774
 Copyright terms: Public domain W3C validator