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

Theorem sseld 3192
Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)
Hypothesis
Ref Expression
sseld.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
sseld  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )

Proof of Theorem sseld
StepHypRef Expression
1 sseld.1 . 2  |-  ( ph  ->  A  C_  B )
2 ssel 3187 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165
This theorem is referenced by:  sselda  3193  sseldd  3194  ssneld  3195  elelpwi  3648  ssbrd  4080  uniopel  4286  onminex  4614  dmrnssfld  4954  nfunv  5301  opelf  5420  fvimacnv  5656  suppssr  5675  ffvelrn  5679  f1imass  5804  exopxfr2  6200  dftpos3  6268  oa00  6573  omordi  6580  omlimcl  6592  omeulem1  6596  nnmordi  6645  mapsn  6825  ixpf  6854  pw2f1olem  6982  pssnn  7097  findcard3  7116  ixpfi2  7170  fissuni  7176  elfiun  7199  dffi3  7200  ordiso2  7246  ordtypelem7  7255  ixpiunwdom  7321  sucprcreg  7329  inf3lem2  7346  cantnfreslem  7393  cantnfp1lem3  7398  cantnfp1  7399  cantnflem1  7407  cantnf  7411  trcl  7426  r1ordg  7466  rankelb  7512  rankuni2b  7541  rankval4  7555  tcrank  7570  cplem1  7575  carduniima  7739  alephfp  7751  kmlem2  7793  isf32lem3  7997  domtriomlem  8084  axdc3lem2  8093  ac6num  8122  zorn2lem7  8145  ttukeylem6  8157  iundom2g  8178  fpwwe2lem13  8280  pwfseqlem3  8298  tskss  8396  tskr1om2  8406  inatsk  8416  gruss  8434  gruel  8441  grur1  8458  prlem934  8673  ltexprlem7  8682  supsr  8750  supmullem2  9737  uzind  10119  iccsplit  10784  fzm1  10878  hashbclem  11406  ccatval2  11448  sqrlem6  11749  isercolllem2  12155  sumrblem  12200  fsumcvg  12201  incexclem  12311  isumrpcl  12318  rpnnen2lem4  12512  saddisj  12672  sadass  12678  bitsshft  12682  smuval2  12689  smupvallem  12690  smu01lem  12692  smueqlem  12697  ramub1lem1  13089  ramub1lem2  13090  firest  13353  mrissmrid  13559  acsfiindd  14296  acsmapd  14297  dirge  14375  issubmnd  14417  issubg2  14652  eqgid  14685  dprdff  15263  dprddisj2  15290  ablfac1c  15322  subrgdvds  15575  issubrg2  15581  lssssr  15726  lssats2  15773  lbspss  15851  lsmelval2  15854  lspprat  15922  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  lpigen  16024  lsmcss  16608  obselocv  16644  unitg  16721  elcls  16826  clsndisj  16828  elcls3  16836  neindisj  16870  lpval  16887  lpsscls  16889  lpss3  16892  maxlp  16894  restntr  16928  ordtbas2  16937  ordtbas  16938  pnfnei  16966  mnfnei  16967  cncls2  17018  lmcnp  17048  lpcls  17108  hauscmplem  17149  2ndcdisj  17198  kgen2ss  17266  txuni2  17276  ptpjpre1  17282  tx1cn  17319  tx2cn  17320  prdstopn  17338  txlm  17358  tgqtop  17419  regr1lem  17446  fgss2  17585  uzfbas  17609  ufilmax  17618  uffix2  17635  ufildr  17642  fmfnfmlem1  17665  fmco  17672  flimrest  17694  fclsopn  17725  fclscf  17736  flimfcls  17737  fclscmpi  17740  alexsubALTlem4  17760  divstgplem  17819  imasf1oxms  18051  prdsbl  18053  metrest  18086  iccntr  18342  reconnlem2  18348  caucfil  18725  caussi  18739  bcthlem5  18766  ovoliunlem1  18877  shft2rab  18883  sca2rab  18887  ovolicc2  18897  vitalilem2  18980  vitalilem5  18983  mbfinf  19036  i1f1lem  19060  mbfi1fseqlem4  19089  itgss  19182  itgcn  19213  c1liplem1  19359  c1lip1  19360  c1lip3  19362  lhop2  19378  lhop  19379  dvcnvrelem1  19380  mpfrcl  19418  ply1remlem  19564  plyexmo  19709  fsumvma  20468  logfaclbnd  20477  subgoablo  20994  sspmval  21325  sspival  21330  sspimsval  21332  sspph  21449  ubthlem1  21465  shsubcl  21816  shorth  21890  elspansn3  22167  elnlfn  22524  elpjrn  22786  sumdmdlem2  23015  ballotlemfc0  23067  ballotlemfcc  23068  ballotlemodife  23072  ballotlemimin  23080  ballotlemsima  23090  supssd  23263  xrofsup  23270  supxrnemnf  23271  tpr2rico  23311  iundisjfi  23378  cntmeas  23568  1stmbfm  23580  2ndmbfm  23581  erdszelem8  23744  eupath2  23919  elfzm12  24023  dedekind  24097  fprodcvg  24153  preddowncl  24267  predfz  24274  trpredtr  24304  trpredmintr  24305  dftrpred3g  24307  trpredrec  24312  wfrlem16  24342  sltres  24389  nodenselem8  24413  axlowdimlem16  24657  axlowdimlem17  24658  axcontlem9  24672  ontgval  24942  onsuct0  24952  supadd  24996  itg2addnclem  25003  itg2addnclem2  25004  oprabex2gpop  25139  efilcp  25655  limfn2  25669  limfn3  25670  islimrs3  25684  islimrs4  25685  supnuf  25732  icccon2  25803  dmrngcmp  25854  cmpmorp  25882  isconcl5ab  26205  bsstrs  26249  nbssntrs  26250  lpss2  26571  ismtyima  26630  isnacs3  26888  aomclem2  27255  kelac1  27264  lindfrn  27394  f1lindf  27395  rngunsnply  27481  dvconstbi  27654  expgrowth  27655  climsuselem1  27836  climsuse  27837  ibliccsinexp  27848  iblioosinexp  27850  stoweidlem57  27909  stoweidlem62  27914  stirlinglem11  27936  fafvelrn  28138  bnj142  29070  bnj1171  29346  bnj1280  29366  lshpkr  29929  psubatN  30566  elpaddn0  30611  pclfinN  30711  osumcllem10N  30776  pexmidlem7N  30787  diael  31855  dia2dimlem12  31887  dicelval1stN  32000  dicelval2nd  32001  dib2dim  32055  dih2dimbALTN  32057  dihlspsnssN  32144  dvh1dim  32254  dvhdimlem  32256  dvh3dim2  32260  dvh3dim3N  32261  lcfrvalsnN  32353  mapdrvallem2  32457  mapdpglem2  32485  mapdindp2  32533  mapdindp3  32534  mapdh9a  32602  hdmapval0  32648  hdmapval3lemN  32652  hdmap10lem  32654  hdmap11lem1  32656  hdmap11lem2  32657  hdmapoc  32746
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator