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

Theorem sseld 3797
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 3792 . 2 (𝐴𝐵 → (𝐶𝐴𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-in 3776  df-ss 3783
This theorem is referenced by:  sselda  3798  sseldd  3799  ssneld  3800  elelpwi  4364  ssbrd  4887  uniopel  5171  exopxfr2  5468  dmrnssfld  5585  preddowncl  5920  nfunv  6130  opelf  6276  fvimacnv  6550  ffvelrn  6575  fnsnr  6652  f1imass  6741  onminex  7233  extmptsuppeq  7549  suppssr  7557  dftpos3  7601  wfrlem16  7662  oa00  7872  omordi  7879  omlimcl  7891  omeulem1  7895  nnmordi  7944  mapsnd  8130  ixpf  8163  pw2f1olem  8299  pssnn  8413  findcard3  8438  ixpfi2  8499  fissuni  8506  elfiun  8571  dffi3  8572  ordiso2  8655  ordtypelem7  8664  ixpiunwdom  8731  inf3lem2  8769  cantnfp1lem3  8820  cantnfp1  8821  cantnflem1  8829  cantnf  8833  trcl  8847  r1ordg  8884  rankelb  8930  rankuni2b  8959  rankval4  8973  tcrank  8990  cplem1  8995  carduniima  9198  alephfp  9210  kmlem2  9254  isf32lem3  9458  domtriomlem  9545  axdc3lem2  9554  ac6num  9582  zorn2lem7  9605  ttukeylem6  9617  iundom2g  9643  fpwwe2lem13  9745  tskss  9861  tskr1om2  9871  inatsk  9881  gruss  9899  gruel  9906  grur1  9923  prlem934  10136  ltexprlem7  10145  supsr  10214  dedekind  10481  supadd  11272  supmullem2  11275  uzind  11731  iccsplit  12524  elfz0add  12658  predfz  12684  fsuppmapnn0fiub  13010  ccatval2  13571  swrdswrd  13680  swrdccatin12lem2a  13705  swrdccatin2  13707  swrdccatin12lem2c  13708  swrdccatin12  13711  cshimadifsn0  13796  sqrlem6  14207  isercolllem2  14615  fsumcvg  14662  isumrpcl  14793  fprodcvg  14877  rpnnen2lem4  15162  fproddvdsd  15275  saddisj  15402  sadass  15408  bitsshft  15412  smuval2  15419  smupvallem  15420  smu01lem  15422  smueqlem  15427  reumodprminv  15722  ramub1lem1  15943  firest  16294  mrissmrid  16502  initoeu2lem0  16863  acsfiindd  17378  acsmapd  17379  dirge  17438  issubmnd  17519  issubg2  17807  eqgid  17844  dprdff  18609  dprddisj2  18636  ablfac1c  18668  subrgdvds  18994  issubrg2  19000  lssssr  19155  lssssrOLD  19156  lssats2  19203  lbspss  19285  lsmelval2  19288  lspprat  19358  lbsextlem2  19364  lbsextlem3  19365  lpigen  19461  mplcoe5lem  19672  psgndiflemB  20150  lsmcss  20243  obselocv  20279  f1lindf  20368  mdetdiaglem  20612  cpmadugsumlemF  20891  toprntopon  20940  elcls  21088  clsndisj  21090  elcls3  21098  neindisj  21132  lpval  21154  lpsscls  21156  lpss3  21159  maxlp  21162  restntr  21197  ordtbas2  21206  ordtbas  21207  pnfnei  21235  mnfnei  21236  cncls2  21288  lmcnp  21319  lpcls  21379  hauscmplem  21420  2ndcdisj  21470  kgen2ss  21569  txuni2  21579  ptpjpre1  21585  tx1cn  21623  tx2cn  21624  prdstopn  21642  txlm  21662  imasnopn  21704  imasncld  21705  imasncls  21706  tgqtop  21726  regr1lem  21753  fgss2  21888  uzfbas  21912  ufilmax  21921  uffix2  21938  ufildr  21945  fmfnfmlem1  21968  fmco  21975  flimrest  21997  fclsopn  22028  fclscf  22039  flimfcls  22040  alexsubALTlem4  22064  qustgplem  22134  imasf1oxms  22504  prdsbl  22506  metrest  22539  iccntr  22834  reconnlem2  22840  caucfil  23291  caussi  23305  bcthlem5  23335  ovoliunlem1  23482  shft2rab  23488  sca2rab  23492  ovolicc2  23502  vitalilem2  23589  vitalilem5  23592  mbfinf  23645  i1f1lem  23669  mbfi1fseqlem4  23698  itgss  23791  itgcn  23822  c1liplem1  23972  c1lip1  23973  c1lip3  23975  ply1remlem  24135  plyexmo  24281  lgamucov  24977  fsumvma  25151  logfaclbnd  25160  axlowdimlem16  26050  axcontlem9  26065  edgupgr  26242  upgredg  26246  subgreldmiedg  26390  upgrres1  26420  crctcshwlkn0lem2  26931  wwlksnred  27028  wwlksnext  27029  clwwlkccatlem  27131  clwwlkf  27195  wwlksubclwwlk  27208  eupth2lems  27410  sspmval  27915  sspimsval  27920  sspphOLD  28037  ubthlem1  28053  shsubcl  28404  shorth  28481  elspansn3  28758  elnlfn  29114  elpjrn  29376  sumdmdlem2  29605  fimarab  29771  supssd  29813  infssd  29814  xrofsup  29859  cmpcref  30241  cntmeas  30613  1stmbfm  30646  2ndmbfm  30647  ballotlemfc0  30878  ballotlemfcc  30879  ballotlemodife  30883  ballotlemimin  30891  bnj1171  31389  bnj1280  31409  mrsubrn  31731  elfzm12  31889  trpredtr  32048  trpredmintr  32049  dftrpred3g  32051  trpredrec  32056  sltres  32134  nosepssdm  32155  nodenselem8  32160  nosupno  32168  nosupbday  32170  ontgval  32745  bj-restuni  33359  lindsenlbs  33715  poimirlem16  33736  poimirlem29  33749  poimirlem30  33750  poimirlem31  33751  itg2addnclem  33771  itg2addnclem2  33772  ftc1anclem7  33801  ismtyima  33911  lshpkr  34895  psubatN  35533  elpaddn0  35578  pclfinN  35678  diael  36821  dia2dimlem12  36853  dicelval1stN  36966  dicelval2nd  36967  dib2dim  37021  dih2dimbALTN  37023  dihlspsnssN  37110  dvh1dim  37220  lcfrvalsnN  37319  mapdrvallem2  37423  mapdpglem2  37451  hdmap10lem  37617  hdmap11lem2  37620  hdmapoc  37709  isnacs3  37772  aomclem2  38123  kelac1  38131  rngunsnply  38241  intabssd  38413  iunrelexp0  38491  rfovcnvf1od  38795  rfovcnvfvd  38798  fsovrfovd  38800  clsk1indlem3  38838  neik0pk1imk0  38842  ntrneineine0lem  38878  ntrneiel2  38881  ntrneikb  38889  ntrneik4w  38895  dvconstbi  39030  expgrowth  39031  climsuselem1  40316  climsuse  40317  limcresiooub  40351  iblsplit  40658  iblspltprt  40665  stoweidlem62  40755  stirlinglem11  40777  fourierdlem41  40841  qndenserrnbllem  40990  sge0fodjrnlem  41109  sssmf  41426  smflimsuplem7  41511  fafvelrn  41756  fafv2elrn  41820  smonoord  41913  iccpartiltu  41930  iccpartigtl  41931  iccpartiun  41942  iccpartdisj  41945  pfxccatin12  41997  pfxccatpfx2  42000  bgoldbtbndlem2  42266  c0rnghm  42478  lidldomn1  42486  lidlmmgm  42490  lidlmsgrp  42491  lidlrng  42492  rnghmsscmap  42539  rngcsect  42545  funcrngcsetc  42563  rhmsscmap  42585  rhmsscrnghm  42591  ringcsect  42596  funcringcsetc  42600  funcringcsetcALTV2lem9  42609  rhmsubclem4  42654  rhmsubcALTVlem4  42672  lincresunit3lem1  42833  setrec1  43003  setis  43009  vsetrec  43014
  Copyright terms: Public domain W3C validator