Theorem sseld 3602

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 3597	. 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 1990   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sselda  3603  sseldd  3604  ssneld  3605  elelpwi  4171  ssbrd  4696  uniopel  4978  exopxfr2  5266  dmrnssfld  5384  preddowncl  5707  nfunv  5921  opelf  6065  fvimacnv  6332  ffvelrn  6357  fnsnb  6432  f1imass  6521  onminex  7007  extmptsuppeq  7319  suppssr  7326  dftpos3  7370  wfrlem16  7430  oa00  7639  omordi  7646  omlimcl  7658  omeulem1  7662  nnmordi  7711  mapsn  7899  ixpf  7930  pw2f1olem  8064  pssnn  8178  findcard3  8203  ixpfi2  8264  fissuni  8271  elfiun  8336  dffi3  8337  ordiso2  8420  ordtypelem7  8429  ixpiunwdom  8496  inf3lem2  8526  cantnfp1lem3  8577  cantnfp1  8578  cantnflem1  8586  cantnf  8590  trcl  8604  r1ordg  8641  rankelb  8687  rankuni2b  8716  rankval4  8730  tcrank  8747  cplem1  8752  carduniima  8919  alephfp  8931  kmlem2  8973  isf32lem3  9177  domtriomlem  9264  axdc3lem2  9273  ac6num  9301  zorn2lem7  9324  ttukeylem6  9336  iundom2g  9362  fpwwe2lem13  9464  tskss  9580  tskr1om2  9590  inatsk  9600  gruss  9618  gruel  9625  grur1  9642  prlem934  9855  ltexprlem7  9864  supsr  9933  dedekind  10200  supadd  10991  supmullem2  10994  uzind  11469  iccsplit  12305  elfz0add  12438  predfz  12464  fsuppmapnn0fiub  12790  fsuppmapnn0fiubOLD  12791  ccatval2  13362  swrdswrd  13460  swrdccatin12lem2a  13485  swrdccatin2  13487  swrdccatin12lem2c  13488  swrdccatin12  13491  cshimadifsn0  13576  sqrlem6  13988  isercolllem2  14396  fsumcvg  14443  isumrpcl  14575  fprodcvg  14660  rpnnen2lem4  14946  fproddvdsd  15059  saddisj  15187  sadass  15193  bitsshft  15197  smuval2  15204  smupvallem  15205  smu01lem  15207  smueqlem  15212  reumodprminv  15509  ramub1lem1  15730  firest  16093  mrissmrid  16301  initoeu2lem0  16663  acsfiindd  17177  acsmapd  17178  dirge  17237  issubmnd  17318  issubg2  17609  eqgid  17646  dprdff  18411  dprddisj2  18438  ablfac1c  18470  subrgdvds  18794  issubrg2  18800  lssssr  18953  lssats2  19000  lbspss  19082  lsmelval2  19085  lspprat  19153  lbsextlem2  19159  lbsextlem3  19160  lpigen  19256  mplcoe5lem  19467  psgndiflemB  19946  lsmcss  20036  obselocv  20072  f1lindf  20161  mdetdiaglem  20404  cpmadugsumlemF  20681  toprntopon  20729  elcls  20877  clsndisj  20879  elcls3  20887  neindisj  20921  lpval  20943  lpsscls  20945  lpss3  20948  maxlp  20951  restntr  20986  ordtbas2  20995  ordtbas  20996  pnfnei  21024  mnfnei  21025  cncls2  21077  lmcnp  21108  lpcls  21168  hauscmplem  21209  2ndcdisj  21259  kgen2ss  21358  txuni2  21368  ptpjpre1  21374  tx1cn  21412  tx2cn  21413  prdstopn  21431  txlm  21451  imasnopn  21493  imasncld  21494  imasncls  21495  tgqtop  21515  regr1lem  21542  fgss2  21678  uzfbas  21702  ufilmax  21711  uffix2  21728  ufildr  21735  fmfnfmlem1  21758  fmco  21765  flimrest  21787  fclsopn  21818  fclscf  21829  flimfcls  21830  alexsubALTlem4  21854  qustgplem  21924  imasf1oxms  22294  prdsbl  22296  metrest  22329  iccntr  22624  reconnlem2  22630  caucfil  23081  caussi  23095  bcthlem5  23125  ovoliunlem1  23270  shft2rab  23276  sca2rab  23280  ovolicc2  23290  vitalilem2  23378  vitalilem5  23381  mbfinf  23432  i1f1lem  23456  mbfi1fseqlem4  23485  itgss  23578  itgcn  23609  c1liplem1  23759  c1lip1  23760  c1lip3  23762  ply1remlem  23922  plyexmo  24068  lgamucov  24764  fsumvma  24938  logfaclbnd  24947  axlowdimlem16  25837  axcontlem9  25852  edgupgr  26029  upgredg  26032  subgreldmiedg  26175  upgrres1  26205  nbusgrvtxm1uvtx  26306  crctcshwlkn0lem2  26703  wwlksnred  26787  wwlksnext  26788  clwwlksf  26915  wwlksubclwwlks  26925  eupth2lems  27098  sspmval  27588  sspimsval  27593  sspph  27710  ubthlem1  27726  shsubcl  28077  shorth  28154  elspansn3  28431  elnlfn  28787  elpjrn  29049  sumdmdlem2  29278  fimarab  29445  supssd  29487  infssd  29488  xrofsup  29533  cmpcref  29917  cntmeas  30289  1stmbfm  30322  2ndmbfm  30323  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemodife  30559  ballotlemimin  30567  bnj142OLD  30794  bnj1171  31068  bnj1280  31088  mrsubrn  31410  elfzm12  31569  trpredtr  31730  trpredmintr  31731  dftrpred3g  31733  trpredrec  31738  sltres  31815  nosepssdm  31836  nodenselem8  31841  nosupno  31849  nosupbday  31851  ontgval  32430  bj-restuni  33050  lindsenlbs  33404  poimirlem16  33425  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  itg2addnclem  33461  itg2addnclem2  33462  ftc1anclem7  33491  ismtyima  33602  lshpkr  34404  psubatN  35041  elpaddn0  35086  pclfinN  35186  diael  36332  dia2dimlem12  36364  dicelval1stN  36477  dicelval2nd  36478  dib2dim  36532  dih2dimbALTN  36534  dihlspsnssN  36621  dvh1dim  36731  lcfrvalsnN  36830  mapdrvallem2  36934  mapdpglem2  36962  hdmap10lem  37131  hdmap11lem2  37134  hdmapoc  37223  isnacs3  37273  aomclem2  37625  kelac1  37633  rngunsnply  37743  intabssd  37916  iunrelexp0  37994  rfovcnvf1od  38298  rfovcnvfvd  38301  fsovrfovd  38303  clsk1indlem3  38341  neik0pk1imk0  38345  ntrneineine0lem  38381  ntrneiel2  38384  ntrneikb  38392  ntrneik4w  38398  dvconstbi  38533  expgrowth  38534  mapsnd  39388  climsuselem1  39839  climsuse  39840  limcresiooub  39874  iblsplit  40182  iblspltprt  40189  stoweidlem62  40279  stirlinglem11  40301  fourierdlem41  40365  qndenserrnbllem  40514  sge0fodjrnlem  40633  sssmf  40947  smflimsuplem7  41032  fafvelrn  41250  smonoord  41341  iccpartiltu  41358  iccpartigtl  41359  iccpartiun  41370  iccpartdisj  41373  pfxccatin12  41425  pfxccatpfx2  41428  bgoldbtbndlem2  41694  c0rnghm  41913  lidldomn1  41921  lidlmmgm  41925  lidlmsgrp  41926  lidlrng  41927  rnghmsscmap  41974  rngcsect  41980  funcrngcsetc  41998  rhmsscmap  42020  rhmsscrnghm  42026  ringcsect  42031  funcringcsetc  42035  funcringcsetcALTV2lem9  42044  rhmsubclem4  42089  rhmsubcALTVlem4  42107  lincresunit3lem1  42268  setrec1  42438  vsetrec  42446