Theorem sseld 3417

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 3412	. 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 1904   C_ wss 3390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404

This theorem is referenced by:  sselda  3418  sseldd  3419  ssneld  3420  elelpwi  3953  ssbrd  4437  uniopel  4705  exopxfr2  4984  dmrnssfld  5099  preddowncl  5414  nfunv  5620  opelf  5757  fvimacnv  6012  ffvelrn  6035  fnsnb  6099  f1imass  6183  onminex  6653  extmptsuppeq  6958  suppssr  6965  dftpos3  7009  wfrlem16  7069  oa00  7278  omordi  7285  omlimcl  7297  omeulem1  7301  nnmordi  7350  mapsn  7531  ixpf  7562  pw2f1olem  7694  pssnn  7808  findcard3  7832  ixpfi2  7890  fissuni  7897  elfiun  7962  dffi3  7963  ordiso2  8048  ordtypelem7  8057  ixpiunwdom  8124  inf3lem2  8152  cantnfp1lem3  8203  cantnfp1  8204  cantnflem1  8212  cantnf  8216  trcl  8230  r1ordg  8267  rankelb  8313  rankuni2b  8342  rankval4  8356  tcrank  8373  cplem1  8378  carduniima  8545  alephfp  8557  kmlem2  8599  isf32lem3  8803  domtriomlem  8890  axdc3lem2  8899  ac6num  8927  zorn2lem7  8950  ttukeylem6  8962  iundom2g  8983  fpwwe2lem13  9085  tskss  9201  tskr1om2  9211  inatsk  9221  gruss  9239  gruel  9246  grur1  9263  prlem934  9476  ltexprlem7  9485  supsr  9554  dedekind  9815  supadd  10597  supmullem2  10600  uzind  11050  iccsplit  11791  elfz0add  11917  predfz  11941  fsuppmapnn0fiub  12241  ccatval2  12774  swrdswrd  12870  swrdccatin12lem2a  12895  swrdccatin2  12897  swrdccatin12lem2c  12898  swrdccatin12  12901  cshimadifsn0  12986  sqrlem6  13388  isercolllem2  13806  fsumcvg  13855  isumrpcl  13978  fprodcvg  14061  rpnnen2lem4  14347  fproddvdsd  14449  saddisj  14518  sadass  14524  bitsshft  14528  smuval2  14535  smupvallem  14536  smu01lem  14538  smueqlem  14543  reumodprminv  14834  ramub1lem1  15063  firest  15409  mrissmrid  15625  initoeu2lem0  15986  acsfiindd  16501  acsmapd  16502  dirge  16561  issubmnd  16642  issubg2  16910  eqgid  16947  dprdff  17723  dprddisj2  17750  ablfac1c  17782  subrgdvds  18100  issubrg2  18106  lssssr  18254  lssats2  18301  lbspss  18383  lsmelval2  18386  lspprat  18454  lbsextlem2  18460  lbsextlem3  18461  lpigen  18557  mplcoe5lem  18768  psgndiflemB  19245  lsmcss  19332  obselocv  19368  f1lindf  19457  mdetdiaglem  19700  cpmadugsumlemF  19977  unitgOLD  20060  elcls  20166  clsndisj  20168  elcls3  20176  neindisj  20210  lpval  20232  lpsscls  20234  lpss3  20237  maxlp  20240  restntr  20275  ordtbas2  20284  ordtbas  20285  pnfnei  20313  mnfnei  20314  cncls2  20366  lmcnp  20397  lpcls  20457  hauscmplem  20498  2ndcdisj  20548  kgen2ss  20647  txuni2  20657  ptpjpre1  20663  tx1cn  20701  tx2cn  20702  prdstopn  20720  txlm  20740  imasnopn  20782  imasncld  20783  imasncls  20784  tgqtop  20804  regr1lem  20831  fgss2  20967  uzfbas  20991  ufilmax  21000  uffix2  21017  ufildr  21024  fmfnfmlem1  21047  fmco  21054  flimrest  21076  fclsopn  21107  fclscf  21118  flimfcls  21119  alexsubALTlem4  21143  qustgplem  21213  imasf1oxms  21582  prdsbl  21584  metrest  21617  iccntr  21917  reconnlem2  21923  caucfil  22331  caussi  22345  bcthlem5  22374  ovoliunlem1  22533  shft2rab  22539  sca2rab  22543  ovolicc2  22554  vitalilem2  22646  vitalilem5  22649  mbfinf  22700  mbfinfOLD  22701  i1f1lem  22726  mbfi1fseqlem4  22755  itgss  22848  itgcn  22879  c1liplem1  23027  c1lip1  23028  c1lip3  23030  ply1remlem  23192  plyexmo  23345  lgamucov  24042  fsumvma  24220  logfaclbnd  24229  axlowdimlem16  25066  axcontlem9  25081  wwlknred  25530  wwlknext  25531  clwlkswlks  25565  clwwlkf  25601  wwlksubclwwlk  25611  nbhashuvtx  25723  eupath2  25787  extwwlkfablem2  25885  subgoablo  26120  sspmval  26453  sspival  26458  sspimsval  26460  sspph  26577  ubthlem1  26593  shsubcl  26954  shorth  27029  elspansn3  27306  elnlfn  27662  elpjrn  27924  sumdmdlem2  28153  fimarab  28320  supssd  28365  infssd  28366  xrofsup  28428  cmpcref  28751  cntmeas  29122  1stmbfm  29155  2ndmbfm  29156  ballotlemfc0  29398  ballotlemfcc  29399  ballotlemodife  29403  ballotlemimin  29411  ballotlemiminOLD  29449  bnj142OLD  29606  bnj1171  29881  bnj1280  29901  mrsubrn  30223  elfzm12  30391  trpredtr  30542  trpredmintr  30543  dftrpred3g  30545  trpredrec  30550  sltres  30622  nodenselem8  30648  ontgval  31162  poimirlem16  32020  poimirlem29  32033  poimirlem30  32034  poimirlem31  32035  itg2addnclem  32057  itg2addnclem2  32058  ftc1anclem7  32087  ismtyima  32199  lshpkr  32754  psubatN  33391  elpaddn0  33436  pclfinN  33536  diael  34682  dia2dimlem12  34714  dicelval1stN  34827  dicelval2nd  34828  dib2dim  34882  dih2dimbALTN  34884  dihlspsnssN  34971  dvh1dim  35081  lcfrvalsnN  35180  mapdrvallem2  35284  mapdpglem2  35312  hdmap10lem  35481  hdmap11lem2  35484  hdmapoc  35573  isnacs3  35623  aomclem2  35984  kelac1  35992  rngunsnply  36110  intabssd  36287  iunrelexp0  36365  dvconstbi  36753  expgrowth  36754  mapsnd  37547  climsuselem1  37783  climsuse  37784  limcresiooub  37820  iblsplit  37940  iblspltprt  37947  stoweidlem62  38035  stoweidlem62OLD  38036  stirlinglem11  38058  fourierdlem41  38123  qndenserrnbllem  38275  sge0fodjrnlem  38372  fafvelrn  38817  smonoord  38863  iccpartiltu  38881  iccpartigtl  38882  iccpartiun  38893  iccpartdisj  38896  bgoldbtbndlem2  39046  pfxccatin12  39113  pfxccatpfx2  39116  edgupgr  39386  upgredg  39389  subgreldmiedg  39519  upgrres1  39544  nbusgrvtxm1uvtx  39642  crctcsh1wlkn0lem2  39989  eupth2lems  40150  uhgraedgrnv  40172  c0rnghm  40421  lidldomn1  40429  lidlmmgm  40433  lidlmsgrp  40434  lidlrng  40435  rnghmsscmap  40484  rngcsect  40490  funcrngcsetc  40508  rhmsscmap  40530  rhmsscrnghm  40536  ringcsect  40541  funcringcsetc  40545  funcringcsetcALTV2lem9  40554  rhmsubclem4  40599  rhmsubcALTVlem4  40618  lincresunit3lem1  40780