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

Theorem sseld 3349
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 3344 . 2  |-  ( A 
C_  B  ->  ( C  e.  A  ->  C  e.  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  sselda  3350  sseldd  3351  ssneld  3352  elelpwi  3811  ssbrd  4255  uniopel  4462  onminex  4789  dmrnssfld  5131  nfunv  5486  opelf  5608  fvimacnv  5847  suppssr  5866  ffvelrn  5870  f1imass  6012  exopxfr2  6413  dftpos3  6499  oa00  6804  omordi  6811  omlimcl  6823  omeulem1  6827  nnmordi  6876  mapsn  7057  ixpf  7086  pw2f1olem  7214  pssnn  7329  findcard3  7352  ixpfi2  7407  fissuni  7413  elfiun  7437  dffi3  7438  ordiso2  7486  ordtypelem7  7495  ixpiunwdom  7561  sucprcreg  7569  inf3lem2  7586  cantnfreslem  7633  cantnfp1lem3  7638  cantnfp1  7639  cantnflem1  7647  cantnf  7651  trcl  7666  r1ordg  7706  rankelb  7752  rankuni2b  7781  rankval4  7795  tcrank  7810  cplem1  7815  carduniima  7979  alephfp  7991  kmlem2  8033  isf32lem3  8237  domtriomlem  8324  axdc3lem2  8333  ac6num  8361  zorn2lem7  8384  ttukeylem6  8396  iundom2g  8417  fpwwe2lem13  8519  tskss  8635  tskr1om2  8645  inatsk  8655  gruss  8673  gruel  8680  grur1  8697  prlem934  8912  ltexprlem7  8921  supsr  8989  supmullem2  9977  uzind  10363  iccsplit  11031  fzm1  11129  ccatval2  11748  sqrlem6  12055  isercolllem2  12461  fsumcvg  12508  isumrpcl  12625  rpnnen2lem4  12819  saddisj  12979  sadass  12985  bitsshft  12989  smuval2  12996  smupvallem  12997  smu01lem  12999  smueqlem  13004  ramub1lem1  13396  firest  13662  mrissmrid  13868  acsfiindd  14605  acsmapd  14606  dirge  14684  issubmnd  14726  issubg2  14961  eqgid  14994  dprdff  15572  dprddisj2  15599  ablfac1c  15631  subrgdvds  15884  issubrg2  15890  lssssr  16031  lssats2  16078  lbspss  16156  lsmelval2  16159  lspprat  16227  lbsextlem2  16233  lbsextlem3  16234  lpigen  16329  lsmcss  16921  obselocv  16957  unitg  17034  elcls  17139  clsndisj  17141  elcls3  17149  neindisj  17183  lpval  17205  lpsscls  17207  lpss3  17210  maxlp  17213  restntr  17248  ordtbas2  17257  ordtbas  17258  pnfnei  17286  mnfnei  17287  cncls2  17339  lmcnp  17370  lpcls  17430  hauscmplem  17471  2ndcdisj  17521  kgen2ss  17589  txuni2  17599  ptpjpre1  17605  tx1cn  17643  tx2cn  17644  prdstopn  17662  txlm  17682  imasnopn  17724  imasncld  17725  imasncls  17726  tgqtop  17746  regr1lem  17773  fgss2  17908  uzfbas  17932  ufilmax  17941  uffix2  17958  ufildr  17965  fmfnfmlem1  17988  fmco  17995  flimrest  18017  fclsopn  18048  fclscf  18059  flimfcls  18060  alexsubALTlem4  18083  divstgplem  18152  imasf1oxms  18521  prdsbl  18523  metrest  18556  iccntr  18854  reconnlem2  18860  caucfil  19238  caussi  19252  bcthlem5  19283  ovoliunlem1  19400  shft2rab  19406  sca2rab  19410  ovolicc2  19420  vitalilem2  19503  vitalilem5  19506  mbfinf  19559  i1f1lem  19583  mbfi1fseqlem4  19612  itgss  19705  itgcn  19736  c1liplem1  19882  c1lip1  19883  c1lip3  19885  ply1remlem  20087  plyexmo  20232  fsumvma  20999  logfaclbnd  21008  eupath2  21704  subgoablo  21901  sspmval  22234  sspival  22239  sspimsval  22241  sspph  22358  ubthlem1  22374  shsubcl  22725  shorth  22799  elspansn3  23076  elnlfn  23433  elpjrn  23695  sumdmdlem2  23924  supssd  24100  xrofsup  24128  cntmeas  24582  1stmbfm  24612  2ndmbfm  24613  sitgclbn  24659  ballotlemfc0  24752  ballotlemfcc  24753  ballotlemodife  24757  ballotlemimin  24765  lgamucov  24824  elfzm12  25114  dedekind  25189  fprodcvg  25258  preddowncl  25473  predfz  25480  trpredtr  25510  trpredmintr  25511  dftrpred3g  25513  trpredrec  25518  wfrlem16  25555  sltres  25621  nodenselem8  25645  axlowdimlem16  25898  axcontlem9  25913  ontgval  26183  supadd  26240  itg2addnclem  26258  itg2addnclem2  26259  ftc1anclem7  26288  ismtyima  26514  isnacs3  26766  aomclem2  27132  kelac1  27140  f1lindf  27271  rngunsnply  27357  dvconstbi  27530  expgrowth  27531  climsuselem1  27711  climsuse  27712  stoweidlem62  27789  stirlinglem11  27811  fafvelrn  28012  elfzelfzadd  28121  swrdswrd  28221  swrdccatin12lem3a  28230  swrdccatin2  28232  swrdccatin12lem3c  28233  swrdccatin12  28236  reumodprminv  28249  uhgraedgrnv  28314  nbhashuvtx  28420  bnj142  29155  bnj1171  29431  bnj1280  29451  lshpkr  29977  psubatN  30614  elpaddn0  30659  pclfinN  30759  diael  31903  dia2dimlem12  31935  dicelval1stN  32048  dicelval2nd  32049  dib2dim  32103  dih2dimbALTN  32105  dihlspsnssN  32192  dvh1dim  32302  lcfrvalsnN  32401  mapdrvallem2  32505  mapdpglem2  32533  hdmap10lem  32702  hdmap11lem2  32705  hdmapoc  32794
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator