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

Theorem sseld 3179
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 3174 . 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 1684    C_ wss 3152
This theorem is referenced by:  sselda  3180  sseldd  3181  ssneld  3182  elelpwi  3635  ssbrd  4064  uniopel  4270  onminex  4598  dmrnssfld  4938  nfunv  5285  opelf  5404  fvimacnv  5640  suppssr  5659  ffvelrn  5663  f1imass  5788  exopxfr2  6184  dftpos3  6252  oa00  6557  omordi  6564  omlimcl  6576  omeulem1  6580  nnmordi  6629  mapsn  6809  ixpf  6838  pw2f1olem  6966  pssnn  7081  findcard3  7100  ixpfi2  7154  fissuni  7160  elfiun  7183  dffi3  7184  ordiso2  7230  ordtypelem7  7239  ixpiunwdom  7305  sucprcreg  7313  inf3lem2  7330  cantnfreslem  7377  cantnfp1lem3  7382  cantnfp1  7383  cantnflem1  7391  cantnf  7395  trcl  7410  r1ordg  7450  rankelb  7496  rankuni2b  7525  rankval4  7539  tcrank  7554  cplem1  7559  carduniima  7723  alephfp  7735  kmlem2  7777  isf32lem3  7981  domtriomlem  8068  axdc3lem2  8077  ac6num  8106  zorn2lem7  8129  ttukeylem6  8141  iundom2g  8162  fpwwe2lem13  8264  pwfseqlem3  8282  tskss  8380  tskr1om2  8390  inatsk  8400  gruss  8418  gruel  8425  grur1  8442  prlem934  8657  ltexprlem7  8666  supsr  8734  supmullem2  9721  uzind  10103  iccsplit  10768  fzm1  10862  hashbclem  11390  ccatval2  11432  sqrlem6  11733  isercolllem2  12139  sumrblem  12184  fsumcvg  12185  incexclem  12295  isumrpcl  12302  rpnnen2lem4  12496  saddisj  12656  sadass  12662  bitsshft  12666  smuval2  12673  smupvallem  12674  smu01lem  12676  smueqlem  12681  ramub1lem1  13073  ramub1lem2  13074  firest  13337  mrissmrid  13543  acsfiindd  14280  acsmapd  14281  dirge  14359  issubmnd  14401  issubg2  14636  eqgid  14669  dprdff  15247  dprddisj2  15274  ablfac1c  15306  subrgdvds  15559  issubrg2  15565  lssssr  15710  lssats2  15757  lbspss  15835  lsmelval2  15838  lspprat  15906  lbsextlem2  15912  lbsextlem3  15913  lbsextlem4  15914  lpigen  16008  lsmcss  16592  obselocv  16628  unitg  16705  elcls  16810  clsndisj  16812  elcls3  16820  neindisj  16854  lpval  16871  lpsscls  16873  lpss3  16876  maxlp  16878  restntr  16912  ordtbas2  16921  ordtbas  16922  pnfnei  16950  mnfnei  16951  cncls2  17002  lmcnp  17032  lpcls  17092  hauscmplem  17133  2ndcdisj  17182  kgen2ss  17250  txuni2  17260  ptpjpre1  17266  tx1cn  17303  tx2cn  17304  prdstopn  17322  txlm  17342  tgqtop  17403  regr1lem  17430  fgss2  17569  uzfbas  17593  ufilmax  17602  uffix2  17619  ufildr  17626  fmfnfmlem1  17649  fmco  17656  flimrest  17678  fclsopn  17709  fclscf  17720  flimfcls  17721  fclscmpi  17724  alexsubALTlem4  17744  divstgplem  17803  imasf1oxms  18035  prdsbl  18037  metrest  18070  iccntr  18326  reconnlem2  18332  caucfil  18709  caussi  18723  bcthlem5  18750  ovoliunlem1  18861  shft2rab  18867  sca2rab  18871  ovolicc2  18881  vitalilem2  18964  vitalilem5  18967  mbfinf  19020  i1f1lem  19044  mbfi1fseqlem4  19073  itgss  19166  itgcn  19197  c1liplem1  19343  c1lip1  19344  c1lip3  19346  lhop2  19362  lhop  19363  dvcnvrelem1  19364  mpfrcl  19402  ply1remlem  19548  plyexmo  19693  fsumvma  20452  logfaclbnd  20461  subgoablo  20978  sspmval  21309  sspival  21314  sspimsval  21316  sspph  21433  ubthlem1  21449  shsubcl  21800  shorth  21874  elspansn3  22151  elnlfn  22508  elpjrn  22770  sumdmdlem2  22999  ballotlemfc0  23051  ballotlemfcc  23052  ballotlemodife  23056  ballotlemimin  23064  ballotlemsima  23074  supssd  23248  xrofsup  23255  supxrnemnf  23256  tpr2rico  23296  iundisjfi  23363  cntmeas  23553  1stmbfm  23565  2ndmbfm  23566  erdszelem8  23729  eupath2  23904  elfzm12  24008  dedekind  24082  preddowncl  24196  predfz  24203  trpredtr  24233  trpredmintr  24234  dftrpred3g  24236  trpredrec  24241  wfrlem16  24271  sltres  24318  nodenselem8  24342  axlowdimlem16  24585  axlowdimlem17  24586  axcontlem9  24600  ontgval  24870  onsuct0  24880  oprabex2gpop  25036  efilcp  25552  limfn2  25566  limfn3  25567  islimrs3  25581  islimrs4  25582  supnuf  25629  icccon2  25700  dmrngcmp  25751  cmpmorp  25779  isconcl5ab  26102  bsstrs  26146  nbssntrs  26147  lpss2  26468  ismtyima  26527  isnacs3  26785  aomclem2  27152  kelac1  27161  lindfrn  27291  f1lindf  27292  rngunsnply  27378  dvconstbi  27551  expgrowth  27552  climsuselem1  27733  climsuse  27734  ibliccsinexp  27745  iblioosinexp  27747  stoweidlem57  27806  stoweidlem62  27811  stirlinglem11  27833  fafvelrn  28032  bnj142  28754  bnj1171  29030  bnj1280  29050  lshpkr  29307  psubatN  29944  elpaddn0  29989  pclfinN  30089  osumcllem10N  30154  pexmidlem7N  30165  diael  31233  dia2dimlem12  31265  dicelval1stN  31378  dicelval2nd  31379  dib2dim  31433  dih2dimbALTN  31435  dihlspsnssN  31522  dvh1dim  31632  dvhdimlem  31634  dvh3dim2  31638  dvh3dim3N  31639  lcfrvalsnN  31731  mapdrvallem2  31835  mapdpglem2  31863  mapdindp2  31911  mapdindp3  31912  mapdh9a  31980  hdmapval0  32026  hdmapval3lemN  32030  hdmap10lem  32032  hdmap11lem1  32034  hdmap11lem2  32035  hdmapoc  32124
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator