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

Theorem sseld 3917
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 3911 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  wss 3884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-in 3891  df-ss 3901
This theorem is referenced by:  sselda  3918  sseldd  3919  ssneld  3920  elelpwi  4512  ssbrd  5076  uniopel  5374  exopxfr2  5683  dmrnssfld  5810  preddowncl  6147  opelf  6517  fvimacnv  6804  ffvelrn  6830  fnsnr  6908  f1imass  7004  onminex  7506  extmptsuppeq  7841  suppssr  7848  dftpos3  7897  wfrlem16  7957  oa00  8172  omordi  8179  omlimcl  8191  omeulem1  8195  nnmordi  8244  mapsnd  8437  ixpf  8471  pw2f1olem  8608  pssnn  8724  findcard3  8749  ixpfi2  8810  fissuni  8817  elfiun  8882  dffi3  8883  ordiso2  8967  ordtypelem7  8976  ixpiunwdom  9042  inf3lem2  9080  cantnfp1lem3  9131  cantnfp1  9132  cantnflem1  9140  cantnf  9144  trcl  9158  r1ordg  9195  rankelb  9241  rankuni2b  9270  rankval4  9284  tcrank  9301  cplem1  9306  carduniima  9511  alephfp  9523  kmlem2  9566  isf32lem3  9770  domtriomlem  9857  axdc3lem2  9866  zorn2lem7  9917  ttukeylem6  9929  iundom2g  9955  fpwwe2lem13  10057  tskss  10173  tskr1om2  10183  inatsk  10193  gruss  10211  gruel  10218  grur1  10235  prlem934  10448  ltexprlem7  10457  supsr  10527  dedekind  10796  supadd  11600  supmullem2  11603  uzind  12066  iccsplit  12867  elfz0add  13005  predfz  13031  fsuppmapnn0fiub  13358  ccatval2  13927  swrdswrd  14062  pfxccatin12lem2a  14084  swrdccatin2  14086  pfxccatpfx2  14094  cshimadifsn0  14187  sqrlem6  14603  isercolllem2  15018  fsumcvg  15065  isumrpcl  15194  fprodcvg  15280  rpnnen2lem4  15566  fproddvdsd  15680  saddisj  15808  sadass  15814  bitsshft  15818  smuval2  15825  smupvallem  15826  smu01lem  15828  smueqlem  15833  reumodprminv  16135  ramub1lem1  16356  firest  16702  mrissmrid  16908  initoeu2lem0  17269  acsfiindd  17783  acsmapd  17784  dirge  17843  issubmnd  17934  issubg2  18290  eqgid  18328  cyccom  18342  dprdff  19131  dprddisj2  19158  ablfac1c  19190  subrgdvds  19546  issubrg2  19552  lssssr  19722  lssats2  19769  lbspss  19851  lsmelval2  19854  lspprat  19922  lbsextlem2  19928  lbsextlem3  19929  lpigen  20026  psgndiflemB  20293  lsmcss  20385  obselocv  20421  f1lindf  20515  issubassa3  20558  mplcoe5lem  20711  mdetdiaglem  21207  cpmadugsumlemF  21485  toprntopon  21534  elcls  21682  clsndisj  21684  elcls3  21692  neindisj  21726  lpval  21748  lpsscls  21750  lpss3  21753  maxlp  21756  restntr  21791  ordtbas2  21800  ordtbas  21801  pnfnei  21829  mnfnei  21830  cncls2  21882  lmcnp  21913  lpcls  21973  hauscmplem  22015  2ndcdisj  22065  kgen2ss  22164  txuni2  22174  ptpjpre1  22180  tx1cn  22218  tx2cn  22219  prdstopn  22237  txlm  22257  imasnopn  22299  imasncld  22300  imasncls  22301  tgqtop  22321  regr1lem  22348  fgss2  22483  uzfbas  22507  ufilmax  22516  uffix2  22533  ufildr  22540  fmfnfmlem1  22563  fmco  22570  flimrest  22592  fclsopn  22623  fclscf  22634  flimfcls  22635  alexsubALTlem4  22659  qustgplem  22730  imasf1oxms  23100  prdsbl  23102  metrest  23135  iccntr  23430  reconnlem2  23436  caucfil  23891  caussi  23905  bcthlem5  23936  ovoliunlem1  24110  shft2rab  24116  sca2rab  24120  ovolicc2  24130  vitalilem2  24217  vitalilem5  24220  mbfinf  24273  i1f1lem  24297  mbfi1fseqlem4  24326  itgss  24419  itgcn  24452  c1liplem1  24603  c1lip1  24604  c1lip3  24606  ply1remlem  24767  plyexmo  24913  lgamucov  25627  fsumvma  25801  logfaclbnd  25810  axlowdimlem16  26755  axcontlem9  26770  edgupgr  26931  upgredg  26934  subgreldmiedg  27077  upgrres1  27107  crctcshwlkn0lem2  27601  wwlksnred  27682  clwwlkccatlem  27778  clwwlkf  27836  wwlksubclwwlk  27847  eupth2lems  28027  sspmval  28520  sspimsval  28525  ubthlem1  28657  shsubcl  29007  shorth  29082  elspansn3  29359  elnlfn  29715  elpjrn  29977  sumdmdlem2  30206  eqrrabd  30276  nfpconfp  30395  fimarab  30408  supssd  30475  infssd  30476  xrofsup  30522  elrspunidl  31018  cmpcref  31207  zarclsiin  31228  cntmeas  31599  1stmbfm  31632  2ndmbfm  31633  ballotlemfc0  31864  ballotlemfcc  31865  ballotlemodife  31869  ballotlemimin  31877  bnj1171  32386  bnj1280  32406  subgrwlk  32493  gonarlem  32755  goalrlem  32757  mrsubrn  32874  elfzm12  33032  trpredtr  33183  trpredmintr  33184  dftrpred3g  33186  trpredrec  33191  sltres  33283  nosepssdm  33304  nodenselem8  33309  nosupno  33317  nosupbday  33319  ontgval  33893  bj-restuni  34513  pibt2  34835  lindsenlbs  35051  poimirlem16  35072  poimirlem29  35085  poimirlem30  35086  poimirlem31  35087  itg2addnclem  35107  itg2addnclem2  35108  ftc1anclem7  35135  ismtyima  35240  lshpkr  36412  psubatN  37050  elpaddn0  37095  pclfinN  37195  diael  38338  dia2dimlem12  38370  dicelval1stN  38483  dicelval2nd  38484  dib2dim  38538  dih2dimbALTN  38540  dihlspsnssN  38627  dvh1dim  38737  lcfrvalsnN  38836  mapdrvallem2  38940  mapdpglem2  38968  hdmap10lem  39134  hdmap11lem2  39137  hdmapoc  39226  isnacs3  39644  aomclem2  39992  kelac1  40000  rngunsnply  40110  intabssd  40220  iunrelexp0  40396  rfovcnvf1od  40698  rfovcnvfvd  40701  fsovrfovd  40703  clsk1indlem3  40739  neik0pk1imk0  40743  ntrneineine0lem  40779  ntrneiel2  40782  ntrneikb  40790  ntrneik4w  40796  mnuop3d  40972  dvconstbi  41031  expgrowth  41032  climsuselem1  42242  climsuse  42243  limcresiooub  42277  iblsplit  42601  iblspltprt  42608  stoweidlem62  42697  stirlinglem11  42719  fourierdlem41  42783  qndenserrnbllem  42929  sge0fodjrnlem  43048  sssmf  43365  smflimsuplem7  43450  fafvelrn  43719  fafv2elrn  43783  smonoord  43881  iccpartiltu  43932  iccpartigtl  43933  iccpartiun  43944  iccpartdisj  43947  bgoldbtbndlem2  44317  c0rnghm  44530  lidldomn1  44538  lidlmmgm  44542  lidlmsgrp  44543  lidlrng  44544  rnghmsscmap  44591  rngcsect  44597  funcrngcsetc  44615  rhmsscmap  44637  rhmsscrnghm  44643  ringcsect  44648  funcringcsetc  44652  funcringcsetcALTV2lem9  44661  rhmsubclem4  44706  rhmsubcALTVlem4  44724  lincresunit3lem1  44881  setrec1  45214  setis  45220  vsetrec  45225
  Copyright terms: Public domain W3C validator