Theorem sseld 3488

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 3483	. 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 1804   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475

This theorem is referenced by:  sselda  3489  sseldd  3490  ssneld  3491  elelpwi  4008  ssbrd  4478  uniopel  4741  exopxfr2  5137  dmrnssfld  5251  nfunv  5609  opelf  5737  fvimacnv  5987  suppssrOLD  6006  ffvelrn  6014  fnsnb  6075  f1imass  6157  onminex  6627  extmptsuppeq  6926  suppssr  6933  dftpos3  6975  oa00  7210  omordi  7217  omlimcl  7229  omeulem1  7233  nnmordi  7282  mapsn  7462  ixpf  7493  pw2f1olem  7623  pssnn  7740  findcard3  7765  ixpfi2  7820  fissuni  7827  elfiun  7892  dffi3  7893  ordiso2  7943  ordtypelem7  7952  ixpiunwdom  8020  sucprcregOLD  8029  inf3lem2  8049  cantnfp1lem3  8102  cantnfp1  8103  cantnflem1  8111  cantnf  8115  cantnfp1lem3OLD  8128  cantnfp1OLD  8129  cantnflem1OLD  8134  cantnfOLD  8137  trcl  8162  r1ordg  8199  rankelb  8245  rankuni2b  8274  rankval4  8288  tcrank  8305  cplem1  8310  carduniima  8480  alephfp  8492  kmlem2  8534  isf32lem3  8738  domtriomlem  8825  axdc3lem2  8834  ac6num  8862  zorn2lem7  8885  ttukeylem6  8897  iundom2g  8918  fpwwe2lem13  9023  tskss  9139  tskr1om2  9149  inatsk  9159  gruss  9177  gruel  9184  grur1  9201  prlem934  9414  ltexprlem7  9423  supsr  9492  dedekind  9747  supmullem2  10517  uzind  10961  iccsplit  11664  fzm1  11769  elfz0add  11786  elfz0addOLD  11787  fsuppmapnn0fiub  12079  ccatval2  12578  swrdswrd  12667  swrdccatin12lem2a  12692  swrdccatin2  12694  swrdccatin12lem2c  12695  swrdccatin12  12698  sqrlem6  13063  isercolllem2  13470  fsumcvg  13516  isumrpcl  13637  fprodcvg  13719  rpnnen2lem4  13933  saddisj  14097  sadass  14103  bitsshft  14107  smuval2  14114  smupvallem  14115  smu01lem  14117  smueqlem  14122  reumodprminv  14311  ramub1lem1  14526  firest  14812  mrissmrid  15020  acsfiindd  15786  acsmapd  15787  dirge  15846  issubmnd  15927  issubg2  16195  eqgid  16232  dprdff  17025  dprdffOLD  17031  dprddisj2  17066  dprddisj2OLD  17067  ablfac1c  17101  subrgdvds  17422  issubrg2  17428  lssssr  17578  lssats2  17625  lbspss  17707  lsmelval2  17710  lspprat  17778  lbsextlem2  17784  lbsextlem3  17785  lpigen  17883  mplcoe5lem  18109  psgndiflemB  18614  lsmcss  18701  obselocv  18737  f1lindf  18835  mdetdiaglem  19078  cpmadugsumlemF  19355  unitgOLD  19447  elcls  19552  clsndisj  19554  elcls3  19562  neindisj  19596  lpval  19618  lpsscls  19620  lpss3  19623  maxlp  19626  restntr  19661  ordtbas2  19670  ordtbas  19671  pnfnei  19699  mnfnei  19700  cncls2  19752  lmcnp  19783  lpcls  19843  hauscmplem  19884  2ndcdisj  19935  kgen2ss  20034  txuni2  20044  ptpjpre1  20050  tx1cn  20088  tx2cn  20089  prdstopn  20107  txlm  20127  imasnopn  20169  imasncld  20170  imasncls  20171  tgqtop  20191  regr1lem  20218  fgss2  20353  uzfbas  20377  ufilmax  20386  uffix2  20403  ufildr  20410  fmfnfmlem1  20433  fmco  20440  flimrest  20462  fclsopn  20493  fclscf  20504  flimfcls  20505  alexsubALTlem4  20528  qustgplem  20597  imasf1oxms  20970  prdsbl  20972  metrest  21005  iccntr  21304  reconnlem2  21310  caucfil  21700  caussi  21714  bcthlem5  21745  ovoliunlem1  21891  shft2rab  21897  sca2rab  21901  ovolicc2  21911  vitalilem2  21996  vitalilem5  21999  mbfinf  22050  i1f1lem  22074  mbfi1fseqlem4  22103  itgss  22196  itgcn  22227  c1liplem1  22375  c1lip1  22376  c1lip3  22378  ply1remlem  22541  plyexmo  22687  fsumvma  23466  logfaclbnd  23475  axlowdimlem16  24238  axcontlem9  24253  wwlknred  24701  wwlknext  24702  clwlkswlks  24736  clwwlkf  24772  wwlksubclwwlk  24782  nbhashuvtx  24894  eupath2  24958  extwwlkfablem2  25056  subgoablo  25291  sspmval  25624  sspival  25629  sspimsval  25631  sspph  25748  ubthlem1  25764  shsubcl  26116  shorth  26191  elspansn3  26468  elnlfn  26825  elpjrn  27087  sumdmdlem2  27316  fimarab  27461  supssd  27505  xrofsup  27560  cmpcref  27831  cntmeas  28175  1stmbfm  28209  2ndmbfm  28210  ballotlemfc0  28409  ballotlemfcc  28410  ballotlemodife  28414  ballotlemimin  28422  lgamucov  28558  mrsubrn  28851  elfzm12  29019  preddowncl  29252  predfz  29259  trpredtr  29289  trpredmintr  29290  dftrpred3g  29292  trpredrec  29297  wfrlem16  29334  sltres  29400  nodenselem8  29424  ontgval  29872  supadd  30018  itg2addnclem  30042  itg2addnclem2  30043  ftc1anclem7  30072  ismtyima  30275  isnacs3  30618  aomclem2  30977  kelac1  30985  rngunsnply  31098  dvconstbi  31215  expgrowth  31216  climsuselem1  31567  climsuse  31568  limcresiooub  31602  iblsplit  31719  iblspltprt  31726  stoweidlem62  31798  stirlinglem11  31820  fourierdlem41  31884  fafvelrn  32209  uhgraedgrnv  32303  lidldomn1  32554  lidlmmgm  32558  lidlmsgrp  32559  lidlrng  32560  rnghmsscmap  32657  rngcsect  32663  funcrngcsetc  32681  rhmsscmap  32700  rhmsscrnghm  32706  ringcsect  32711  funcringcsetc  32715  funcringcsetcOLD2lem9  32724  rhmsubclem4  32765  rhmsubcOLDlem4  32784  lincresunit3lem1  32950  bnj142OLD  33649  bnj1171  33924  bnj1280  33944  lshpkr  34717  psubatN  35354  elpaddn0  35399  pclfinN  35499  diael  36645  dia2dimlem12  36677  dicelval1stN  36790  dicelval2nd  36791  dib2dim  36845  dih2dimbALTN  36847  dihlspsnssN  36934  dvh1dim  37044  lcfrvalsnN  37143  mapdrvallem2  37247  mapdpglem2  37275  hdmap10lem  37444  hdmap11lem2  37447  hdmapoc  37536