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

Theorem sseld 3943
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 3937 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  wss 3910
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927
This theorem is referenced by:  sselda  3944  sseldd  3945  ssneld  3946  elelpwi  4570  ssbrd  5148  uniopel  5473  exopxfr2  5800  dmrnssfld  5925  preddowncl  6286  opelf  6703  elfvunirn  6874  fvimacnv  7003  ffvelcdm  7032  fnsnr  7111  f1imass  7211  onminex  7737  xpord2pred  8077  extmptsuppeq  8119  suppssr  8127  suppssrg  8128  dftpos3  8175  wfrlem16OLD  8270  oa00  8506  omordi  8513  omlimcl  8525  omeulem1  8529  nnmordi  8578  mapsnd  8824  ixpf  8858  pw2f1olem  9020  pssnn  9112  pssnnOLD  9209  findcard3  9229  findcard3OLD  9230  ixpfi2  9294  fissuni  9301  elfiun  9366  dffi3  9367  ordiso2  9451  ordtypelem7  9460  ixpiunwdom  9526  inf3lem2  9565  cantnfp1lem3  9616  cantnfp1  9617  cantnflem1  9625  cantnf  9629  trcl  9664  r1ordg  9714  rankelb  9760  rankuni2b  9789  rankval4  9803  tcrank  9820  cplem1  9825  carduniima  10032  alephfp  10044  kmlem2  10087  isf32lem3  10291  domtriomlem  10378  axdc3lem2  10387  zorn2lem7  10438  ttukeylem6  10450  iundom2g  10476  fpwwe2lem12  10578  tskss  10694  tskr1om2  10704  inatsk  10714  gruss  10732  gruel  10739  grur1  10756  prlem934  10969  ltexprlem7  10978  supsr  11048  dedekind  11318  supadd  12123  supmullem2  12126  uzind  12595  iccsplit  13402  elfz0add  13540  predfz  13566  fsuppmapnn0fiub  13896  ccatval2  14466  swrdswrd  14593  pfxccatin12lem2a  14615  swrdccatin2  14617  pfxccatpfx2  14625  cshimadifsn0  14719  01sqrexlem6  15132  isercolllem2  15550  fsumcvg  15597  isumrpcl  15728  fprodcvg  15813  rpnnen2lem4  16099  fproddvdsd  16217  saddisj  16345  sadass  16351  bitsshft  16355  smuval2  16362  smupvallem  16363  smu01lem  16365  smueqlem  16370  reumodprminv  16676  ramub1lem1  16898  firest  17314  mrissmrid  17521  initoeu2lem0  17899  acsfiindd  18442  acsmapd  18443  dirge  18492  issubmnd  18583  issubg2  18943  eqgid  18982  cyccom  18996  dprdff  19791  dprddisj2  19818  ablfac1c  19850  subrgdvds  20236  issubrg2  20242  lssssr  20414  lssats2  20461  lbspss  20543  lsmelval2  20546  lspprat  20614  lbsextlem2  20620  lbsextlem3  20621  lpigen  20726  psgndiflemB  21004  lsmcss  21096  obselocv  21134  f1lindf  21228  issubassa3  21271  mplcoe5lem  21440  mdetdiaglem  21947  cpmadugsumlemF  22225  toprntopon  22274  elcls  22424  clsndisj  22426  elcls3  22434  neindisj  22468  lpval  22490  lpsscls  22492  lpss3  22495  maxlp  22498  restntr  22533  ordtbas2  22542  ordtbas  22543  pnfnei  22571  mnfnei  22572  cncls2  22624  lmcnp  22655  lpcls  22715  hauscmplem  22757  2ndcdisj  22807  kgen2ss  22906  txuni2  22916  ptpjpre1  22922  tx1cn  22960  tx2cn  22961  prdstopn  22979  txlm  22999  imasnopn  23041  imasncld  23042  imasncls  23043  tgqtop  23063  regr1lem  23090  fgss2  23225  uzfbas  23249  ufilmax  23258  uffix2  23275  ufildr  23282  fmfnfmlem1  23305  fmco  23312  flimrest  23334  fclsopn  23365  fclscf  23376  flimfcls  23377  alexsubALTlem4  23401  qustgplem  23472  imasf1oxms  23845  prdsbl  23847  metrest  23880  iccntr  24184  reconnlem2  24190  caucfil  24647  caussi  24661  bcthlem5  24692  ovoliunlem1  24866  shft2rab  24872  sca2rab  24876  ovolicc2  24886  vitalilem2  24973  vitalilem5  24976  mbfinf  25029  i1f1lem  25053  mbfi1fseqlem4  25083  itgss  25176  itgcn  25209  c1liplem1  25360  c1lip1  25361  c1lip3  25363  ply1remlem  25527  plyexmo  25673  lgamucov  26387  fsumvma  26561  logfaclbnd  26570  sltres  27010  nosepssdm  27034  nodenselem8  27039  nosupno  27051  nosupbday  27053  noinfbday  27068  elmade  27197  oldssmade  27207  axlowdimlem16  27906  axcontlem9  27921  edgupgr  28085  upgredg  28088  subgreldmiedg  28231  upgrres1  28261  crctcshwlkn0lem2  28756  wwlksnred  28837  clwwlkccatlem  28933  clwwlkf  28991  wwlksubclwwlk  29002  eupth2lems  29182  sspmval  29675  sspimsval  29680  ubthlem1  29812  shsubcl  30162  shorth  30237  elspansn3  30514  elnlfn  30870  elpjrn  31132  sumdmdlem2  31361  eqrrabd  31430  nfpconfp  31546  fimarab  31559  supssd  31626  infssd  31627  xrofsup  31672  elrspunidl  32203  ressply1mon1p  32278  cmpcref  32431  zarclsiin  32452  cntmeas  32825  1stmbfm  32860  2ndmbfm  32861  ballotlemfc0  33092  ballotlemfcc  33093  ballotlemodife  33097  ballotlemimin  33105  bnj1171  33612  bnj1280  33632  subgrwlk  33726  gonarlem  33988  goalrlem  33990  mrsubrn  34107  elfzm12  34263  ontgval  34903  bj-restuni  35568  pibt2  35888  lindsenlbs  36073  poimirlem29  36107  poimirlem30  36108  poimirlem31  36109  itg2addnclem  36129  itg2addnclem2  36130  ftc1anclem7  36157  ismtyima  36262  lshpkr  37579  psubatN  38218  elpaddn0  38263  pclfinN  38363  diael  39506  dia2dimlem12  39538  dicelval1stN  39651  dicelval2nd  39652  dib2dim  39706  dih2dimbALTN  39708  dihlspsnssN  39795  dvh1dim  39905  lcfrvalsnN  40004  mapdrvallem2  40108  mapdpglem2  40136  hdmap10lem  40302  hdmap11lem2  40305  hdmapoc  40394  sticksstones3  40556  sticksstones17  40571  sticksstones18  40572  isnacs3  41019  aomclem2  41368  kelac1  41376  rngunsnply  41486  safesnsupfiub  41678  intabssd  41781  iunrelexp0  41964  rfovcnvf1od  42266  rfovcnvfvd  42269  fsovrfovd  42271  clsk1indlem3  42305  neik0pk1imk0  42309  ntrneineine0lem  42345  ntrneiel2  42348  ntrneikb  42356  ntrneik4w  42362  mnuop3d  42541  dvconstbi  42604  expgrowth  42605  climsuselem1  43838  climsuse  43839  limcresiooub  43873  iblsplit  44197  iblspltprt  44204  stoweidlem62  44293  stirlinglem11  44315  fourierdlem41  44379  qndenserrnbllem  44525  sge0fodjrnlem  44647  sssmf  44969  smflimsuplem7  45057  fafvelcdm  45392  fafv2elcdm  45456  smonoord  45553  iccpartiltu  45604  iccpartigtl  45605  iccpartiun  45616  iccpartdisj  45619  bgoldbtbndlem2  45988  c0rnghm  46201  lidldomn1  46209  lidlmmgm  46213  lidlmsgrp  46214  lidlrng  46215  rnghmsscmap  46262  rngcsect  46268  funcrngcsetc  46286  rhmsscmap  46308  rhmsscrnghm  46314  ringcsect  46319  funcringcsetc  46323  funcringcsetcALTV2lem9  46332  rhmsubclem4  46377  rhmsubcALTVlem4  46395  lincresunit3lem1  46550  setrec1  47126  setis  47133  vsetrec  47138  pgindnf  47151
  Copyright terms: Public domain W3C validator