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  4256  uniopel  4463  onminex  4790  dmrnssfld  5132  nfunv  5487  opelf  5609  fvimacnv  5848  suppssr  5867  ffvelrn  5871  f1imass  6013  exopxfr2  6414  dftpos3  6500  oa00  6805  omordi  6812  omlimcl  6824  omeulem1  6828  nnmordi  6877  mapsn  7058  ixpf  7087  pw2f1olem  7215  pssnn  7330  findcard3  7353  ixpfi2  7408  fissuni  7414  elfiun  7438  dffi3  7439  ordiso2  7487  ordtypelem7  7496  ixpiunwdom  7562  sucprcreg  7570  inf3lem2  7587  cantnfreslem  7634  cantnfp1lem3  7639  cantnfp1  7640  cantnflem1  7648  cantnf  7652  trcl  7667  r1ordg  7707  rankelb  7753  rankuni2b  7782  rankval4  7796  tcrank  7813  cplem1  7818  carduniima  7982  alephfp  7994  kmlem2  8036  isf32lem3  8240  domtriomlem  8327  axdc3lem2  8336  ac6num  8364  zorn2lem7  8387  ttukeylem6  8399  iundom2g  8420  fpwwe2lem13  8522  tskss  8638  tskr1om2  8648  inatsk  8658  gruss  8676  gruel  8683  grur1  8700  prlem934  8915  ltexprlem7  8924  supsr  8992  supmullem2  9980  uzind  10366  iccsplit  11034  fzm1  11132  ccatval2  11751  sqrlem6  12058  isercolllem2  12464  fsumcvg  12511  isumrpcl  12628  rpnnen2lem4  12822  saddisj  12982  sadass  12988  bitsshft  12992  smuval2  12999  smupvallem  13000  smu01lem  13002  smueqlem  13007  ramub1lem1  13399  firest  13665  mrissmrid  13871  acsfiindd  14608  acsmapd  14609  dirge  14687  issubmnd  14729  issubg2  14964  eqgid  14997  dprdff  15575  dprddisj2  15602  ablfac1c  15634  subrgdvds  15887  issubrg2  15893  lssssr  16034  lssats2  16081  lbspss  16159  lsmelval2  16162  lspprat  16230  lbsextlem2  16236  lbsextlem3  16237  lpigen  16332  lsmcss  16924  obselocv  16960  unitg  17037  elcls  17142  clsndisj  17144  elcls3  17152  neindisj  17186  lpval  17208  lpsscls  17210  lpss3  17213  maxlp  17216  restntr  17251  ordtbas2  17260  ordtbas  17261  pnfnei  17289  mnfnei  17290  cncls2  17342  lmcnp  17373  lpcls  17433  hauscmplem  17474  2ndcdisj  17524  kgen2ss  17592  txuni2  17602  ptpjpre1  17608  tx1cn  17646  tx2cn  17647  prdstopn  17665  txlm  17685  imasnopn  17727  imasncld  17728  imasncls  17729  tgqtop  17749  regr1lem  17776  fgss2  17911  uzfbas  17935  ufilmax  17944  uffix2  17961  ufildr  17968  fmfnfmlem1  17991  fmco  17998  flimrest  18020  fclsopn  18051  fclscf  18062  flimfcls  18063  alexsubALTlem4  18086  divstgplem  18155  imasf1oxms  18524  prdsbl  18526  metrest  18559  iccntr  18857  reconnlem2  18863  caucfil  19241  caussi  19255  bcthlem5  19286  ovoliunlem1  19403  shft2rab  19409  sca2rab  19413  ovolicc2  19423  vitalilem2  19506  vitalilem5  19509  mbfinf  19560  i1f1lem  19584  mbfi1fseqlem4  19613  itgss  19706  itgcn  19737  c1liplem1  19885  c1lip1  19886  c1lip3  19888  ply1remlem  20090  plyexmo  20235  fsumvma  21002  logfaclbnd  21011  eupath2  21707  subgoablo  21904  sspmval  22237  sspival  22242  sspimsval  22244  sspph  22361  ubthlem1  22377  shsubcl  22728  shorth  22802  elspansn3  23079  elnlfn  23436  elpjrn  23698  sumdmdlem2  23927  supssd  24103  xrofsup  24131  cntmeas  24585  1stmbfm  24615  2ndmbfm  24616  sitgclbn  24662  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemodife  24760  ballotlemimin  24768  lgamucov  24827  elfzm12  25117  dedekind  25192  fprodcvg  25261  preddowncl  25476  predfz  25483  trpredtr  25513  trpredmintr  25514  dftrpred3g  25516  trpredrec  25521  wfrlem16  25558  sltres  25624  nodenselem8  25648  axlowdimlem16  25901  axcontlem9  25916  ontgval  26186  supadd  26246  itg2addnclem  26269  itg2addnclem2  26270  ftc1anclem7  26299  ismtyima  26525  isnacs3  26777  aomclem2  27143  kelac1  27151  f1lindf  27282  rngunsnply  27368  dvconstbi  27541  expgrowth  27542  climsuselem1  27722  climsuse  27723  stoweidlem62  27800  stirlinglem11  27822  fafvelrn  28023  elfzelfzadd  28132  swrdswrd  28232  swrdccatin12lem3a  28241  swrdccatin2  28243  swrdccatin12lem3c  28244  swrdccatin12  28247  reumodprminv  28260  uhgraedgrnv  28325  nbhashuvtx  28431  bnj142  29166  bnj1171  29442  bnj1280  29462  lshpkr  29988  psubatN  30625  elpaddn0  30670  pclfinN  30770  diael  31914  dia2dimlem12  31946  dicelval1stN  32059  dicelval2nd  32060  dib2dim  32114  dih2dimbALTN  32116  dihlspsnssN  32203  dvh1dim  32313  lcfrvalsnN  32412  mapdrvallem2  32516  mapdpglem2  32544  hdmap10lem  32713  hdmap11lem2  32716  hdmapoc  32805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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