Theorem sseld 3469

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

Step	Hyp	Ref	Expression
1		sseld.1	. 2 |- ( ph -> A C_ B )
2		ssel 3464	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
3	1, 2	syl 17	1 |- ( ph -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   e. wcel 1870   C_ wss 3442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456

This theorem is referenced by:  sselda  3470  sseldd  3471  ssneld  3472  elelpwi  3996  ssbrd  4467  uniopel  4725  exopxfr2  4999  dmrnssfld  5113  preddowncl  5426  nfunv  5632  opelf  5762  fvimacnv  6012  ffvelrn  6035  fnsnb  6098  f1imass  6180  onminex  6648  extmptsuppeq  6950  suppssr  6957  dftpos3  6999  wfrlem16  7059  oa00  7268  omordi  7275  omlimcl  7287  omeulem1  7291  nnmordi  7340  mapsn  7521  ixpf  7552  pw2f1olem  7682  pssnn  7796  findcard3  7820  ixpfi2  7878  fissuni  7885  elfiun  7950  dffi3  7951  ordiso2  8030  ordtypelem7  8039  ixpiunwdom  8106  inf3lem2  8134  cantnfp1lem3  8184  cantnfp1  8185  cantnflem1  8193  cantnf  8197  trcl  8211  r1ordg  8248  rankelb  8294  rankuni2b  8323  rankval4  8337  tcrank  8354  cplem1  8359  carduniima  8525  alephfp  8537  kmlem2  8579  isf32lem3  8783  domtriomlem  8870  axdc3lem2  8879  ac6num  8907  zorn2lem7  8930  ttukeylem6  8942  iundom2g  8963  fpwwe2lem13  9066  tskss  9182  tskr1om2  9192  inatsk  9202  gruss  9220  gruel  9227  grur1  9244  prlem934  9457  ltexprlem7  9466  supsr  9535  dedekind  9796  supadd  10575  supmullem2  10578  uzind  11027  iccsplit  11763  elfz0add  11889  elfz0addOLD  11890  predfz  11912  fsuppmapnn0fiub  12200  ccatval2  12710  swrdswrd  12801  swrdccatin12lem2a  12826  swrdccatin2  12828  swrdccatin12lem2c  12829  swrdccatin12  12832  sqrlem6  13290  isercolllem2  13707  fsumcvg  13756  isumrpcl  13879  fprodcvg  13962  rpnnen2lem4  14248  fproddvdsd  14348  saddisj  14413  sadass  14419  bitsshft  14423  smuval2  14430  smupvallem  14431  smu01lem  14433  smueqlem  14438  reumodprminv  14718  ramub1lem1  14947  firest  15290  mrissmrid  15498  initoeu2lem0  15859  acsfiindd  16374  acsmapd  16375  dirge  16434  issubmnd  16515  issubg2  16783  eqgid  16820  dprdff  17580  dprddisj2  17607  ablfac1c  17639  subrgdvds  17957  issubrg2  17963  lssssr  18111  lssats2  18158  lbspss  18240  lsmelval2  18243  lspprat  18311  lbsextlem2  18317  lbsextlem3  18318  lpigen  18415  mplcoe5lem  18626  psgndiflemB  19099  lsmcss  19186  obselocv  19222  f1lindf  19311  mdetdiaglem  19554  cpmadugsumlemF  19831  unitgOLD  19914  elcls  20020  clsndisj  20022  elcls3  20030  neindisj  20064  lpval  20086  lpsscls  20088  lpss3  20091  maxlp  20094  restntr  20129  ordtbas2  20138  ordtbas  20139  pnfnei  20167  mnfnei  20168  cncls2  20220  lmcnp  20251  lpcls  20311  hauscmplem  20352  2ndcdisj  20402  kgen2ss  20501  txuni2  20511  ptpjpre1  20517  tx1cn  20555  tx2cn  20556  prdstopn  20574  txlm  20594  imasnopn  20636  imasncld  20637  imasncls  20638  tgqtop  20658  regr1lem  20685  fgss2  20820  uzfbas  20844  ufilmax  20853  uffix2  20870  ufildr  20877  fmfnfmlem1  20900  fmco  20907  flimrest  20929  fclsopn  20960  fclscf  20971  flimfcls  20972  alexsubALTlem4  20996  qustgplem  21066  imasf1oxms  21435  prdsbl  21437  metrest  21470  iccntr  21750  reconnlem2  21756  caucfil  22146  caussi  22160  bcthlem5  22189  ovoliunlem1  22333  shft2rab  22339  sca2rab  22343  ovolicc2  22353  vitalilem2  22444  vitalilem5  22447  mbfinf  22498  mbfinfOLD  22499  i1f1lem  22524  mbfi1fseqlem4  22553  itgss  22646  itgcn  22677  c1liplem1  22825  c1lip1  22826  c1lip3  22828  ply1remlem  22988  plyexmo  23134  lgamucov  23828  fsumvma  24004  logfaclbnd  24013  axlowdimlem16  24833  axcontlem9  24848  wwlknred  25296  wwlknext  25297  clwlkswlks  25331  clwwlkf  25367  wwlksubclwwlk  25377  nbhashuvtx  25489  eupath2  25553  extwwlkfablem2  25651  subgoablo  25884  sspmval  26217  sspival  26222  sspimsval  26224  sspph  26341  ubthlem1  26357  shsubcl  26708  shorth  26783  elspansn3  27060  elnlfn  27416  elpjrn  27678  sumdmdlem2  27907  fimarab  28084  supssd  28130  xrofsup  28189  cmpcref  28516  cntmeas  28887  1stmbfm  28921  2ndmbfm  28922  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemodife  29156  ballotlemimin  29164  bnj142OLD  29322  bnj1171  29597  bnj1280  29617  mrsubrn  29939  elfzm12  30107  trpredtr  30258  trpredmintr  30259  dftrpred3g  30261  trpredrec  30266  sltres  30338  nodenselem8  30362  ontgval  30876  poimirlem16  31659  poimirlem29  31672  poimirlem30  31673  poimirlem31  31674  itg2addnclem  31696  itg2addnclem2  31697  ftc1anclem7  31726  ismtyima  31838  lshpkr  32391  psubatN  33028  elpaddn0  33073  pclfinN  33173  diael  34319  dia2dimlem12  34351  dicelval1stN  34464  dicelval2nd  34465  dib2dim  34519  dih2dimbALTN  34521  dihlspsnssN  34608  dvh1dim  34718  lcfrvalsnN  34817  mapdrvallem2  34921  mapdpglem2  34949  hdmap10lem  35118  hdmap11lem2  35121  hdmapoc  35210  isnacs3  35260  aomclem2  35618  kelac1  35626  rngunsnply  35737  iunrelexp0  35932  dvconstbi  36319  expgrowth  36320  climsuselem1  37257  climsuse  37258  limcresiooub  37294  iblsplit  37411  iblspltprt  37418  stoweidlem62  37491  stoweidlem62OLD  37492  stirlinglem11  37514  fourierdlem41  37578  sge0fodjrnlem  37791  fafvelrn  38061  smonoord  38107  iccpartiltu  38125  iccpartigtl  38126  iccpartiun  38137  iccpartdisj  38140  bgoldbtbndlem2  38290  pfxccatin12  38355  pfxccatpfx2  38358  uhgraedgrnv  38418  c0rnghm  38670  lidldomn1  38678  lidlmmgm  38682  lidlmsgrp  38683  lidlrng  38684  rnghmsscmap  38733  rngcsect  38739  funcrngcsetc  38757  rhmsscmap  38779  rhmsscrnghm  38785  ringcsect  38790  funcringcsetc  38794  funcringcsetcALTV2lem9  38803  rhmsubclem4  38848  rhmsubcALTVlem4  38867  lincresunit3lem1  39031