Theorem sseld 3416

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 3411	. 2 |- ( A C_ B -> ( C e. A -> C e. B ) )
3	1, 2	syl 16	1 |- ( ph -> ( C e. A -> C e. B ) )

Syntax hints:   -> wi 4   e. wcel 1826   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403

This theorem is referenced by:  sselda  3417  sseldd  3418  ssneld  3419  elelpwi  3938  ssbrd  4408  uniopel  4665  exopxfr2  5060  dmrnssfld  5174  nfunv  5527  opelf  5655  fvimacnv  5904  suppssrOLD  5923  ffvelrn  5931  fnsnb  5992  f1imass  6073  onminex  6541  extmptsuppeq  6842  suppssr  6849  dftpos3  6891  oa00  7126  omordi  7133  omlimcl  7145  omeulem1  7149  nnmordi  7198  mapsn  7379  ixpf  7410  pw2f1olem  7540  pssnn  7654  findcard3  7678  ixpfi2  7733  fissuni  7740  elfiun  7805  dffi3  7806  ordiso2  7855  ordtypelem7  7864  ixpiunwdom  7932  inf3lem2  7960  cantnfp1lem3  8012  cantnfp1  8013  cantnflem1  8021  cantnf  8025  cantnfp1lem3OLD  8038  cantnfp1OLD  8039  cantnflem1OLD  8044  cantnfOLD  8047  trcl  8072  r1ordg  8109  rankelb  8155  rankuni2b  8184  rankval4  8198  tcrank  8215  cplem1  8220  carduniima  8390  alephfp  8402  kmlem2  8444  isf32lem3  8648  domtriomlem  8735  axdc3lem2  8744  ac6num  8772  zorn2lem7  8795  ttukeylem6  8807  iundom2g  8828  fpwwe2lem13  8931  tskss  9047  tskr1om2  9057  inatsk  9067  gruss  9085  gruel  9092  grur1  9109  prlem934  9322  ltexprlem7  9331  supsr  9400  dedekind  9655  supmullem2  10426  uzind  10871  iccsplit  11574  elfz0add  11697  elfz0addOLD  11698  fsuppmapnn0fiub  12000  ccatval2  12505  swrdswrd  12596  swrdccatin12lem2a  12621  swrdccatin2  12623  swrdccatin12lem2c  12624  swrdccatin12  12627  sqrlem6  13083  isercolllem2  13490  fsumcvg  13536  isumrpcl  13657  fprodcvg  13739  rpnnen2lem4  13953  saddisj  14117  sadass  14123  bitsshft  14127  smuval2  14134  smupvallem  14135  smu01lem  14137  smueqlem  14142  reumodprminv  14331  ramub1lem1  14546  firest  14840  mrissmrid  15048  initoeu2lem0  15409  acsfiindd  15924  acsmapd  15925  dirge  15984  issubmnd  16065  issubg2  16333  eqgid  16370  dprdff  17159  dprdffOLD  17165  dprddisj2  17200  dprddisj2OLD  17201  ablfac1c  17235  subrgdvds  17556  issubrg2  17562  lssssr  17712  lssats2  17759  lbspss  17841  lsmelval2  17844  lspprat  17912  lbsextlem2  17918  lbsextlem3  17919  lpigen  18017  mplcoe5lem  18243  psgndiflemB  18727  lsmcss  18814  obselocv  18850  f1lindf  18942  mdetdiaglem  19185  cpmadugsumlemF  19462  unitgOLD  19554  elcls  19660  clsndisj  19662  elcls3  19670  neindisj  19704  lpval  19726  lpsscls  19728  lpss3  19731  maxlp  19734  restntr  19769  ordtbas2  19778  ordtbas  19779  pnfnei  19807  mnfnei  19808  cncls2  19860  lmcnp  19891  lpcls  19951  hauscmplem  19992  2ndcdisj  20042  kgen2ss  20141  txuni2  20151  ptpjpre1  20157  tx1cn  20195  tx2cn  20196  prdstopn  20214  txlm  20234  imasnopn  20276  imasncld  20277  imasncls  20278  tgqtop  20298  regr1lem  20325  fgss2  20460  uzfbas  20484  ufilmax  20493  uffix2  20510  ufildr  20517  fmfnfmlem1  20540  fmco  20547  flimrest  20569  fclsopn  20600  fclscf  20611  flimfcls  20612  alexsubALTlem4  20635  qustgplem  20704  imasf1oxms  21077  prdsbl  21079  metrest  21112  iccntr  21411  reconnlem2  21417  caucfil  21807  caussi  21821  bcthlem5  21852  ovoliunlem1  21998  shft2rab  22004  sca2rab  22008  ovolicc2  22018  vitalilem2  22103  vitalilem5  22106  mbfinf  22157  i1f1lem  22181  mbfi1fseqlem4  22210  itgss  22303  itgcn  22334  c1liplem1  22482  c1lip1  22483  c1lip3  22485  ply1remlem  22648  plyexmo  22794  fsumvma  23605  logfaclbnd  23614  axlowdimlem16  24381  axcontlem9  24396  wwlknred  24844  wwlknext  24845  clwlkswlks  24879  clwwlkf  24915  wwlksubclwwlk  24925  nbhashuvtx  25037  eupath2  25101  extwwlkfablem2  25199  subgoablo  25430  sspmval  25763  sspival  25768  sspimsval  25770  sspph  25887  ubthlem1  25903  shsubcl  26255  shorth  26330  elspansn3  26607  elnlfn  26963  elpjrn  27225  sumdmdlem2  27454  fimarab  27623  supssd  27675  xrofsup  27735  cmpcref  28007  cntmeas  28353  1stmbfm  28387  2ndmbfm  28388  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemodife  28619  ballotlemimin  28627  lgamucov  28769  mrsubrn  29062  elfzm12  29230  preddowncl  29441  predfz  29448  trpredtr  29478  trpredmintr  29479  dftrpred3g  29481  trpredrec  29486  wfrlem16  29523  sltres  29589  nodenselem8  29613  ontgval  30049  supadd  30207  itg2addnclem  30232  itg2addnclem2  30233  ftc1anclem7  30262  ismtyima  30465  isnacs3  30808  aomclem2  31167  kelac1  31175  rngunsnply  31290  dvconstbi  31407  expgrowth  31408  climsuselem1  31779  climsuse  31780  limcresiooub  31814  iblsplit  31931  iblspltprt  31938  stoweidlem62  32010  stirlinglem11  32032  fourierdlem41  32096  fafvelrn  32421  pfxccatin12  32600  pfxccatpfx2  32603  uhgraedgrnv  32667  c0rnghm  32919  lidldomn1  32927  lidlmmgm  32931  lidlmsgrp  32932  lidlrng  32933  rnghmsscmap  32982  rngcsect  32988  funcrngcsetc  33006  rhmsscmap  33028  rhmsscrnghm  33034  ringcsect  33039  funcringcsetc  33043  funcringcsetcALTV2lem9  33052  rhmsubclem4  33097  rhmsubcALTVlem4  33116  lincresunit3lem1  33280  bnj142OLD  34128  bnj1171  34403  bnj1280  34423  lshpkr  35255  psubatN  35892  elpaddn0  35937  pclfinN  36037  diael  37183  dia2dimlem12  37215  dicelval1stN  37328  dicelval2nd  37329  dib2dim  37383  dih2dimbALTN  37385  dihlspsnssN  37472  dvh1dim  37582  lcfrvalsnN  37681  mapdrvallem2  37785  mapdpglem2  37813  hdmap10lem  37982  hdmap11lem2  37985  hdmapoc  38074  iunrelexp0  38242