Theorem sseld 3463

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 3458	. 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 1872   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450

This theorem is referenced by:  sselda  3464  sseldd  3465  ssneld  3466  elelpwi  3992  ssbrd  4465  uniopel  4724  exopxfr2  4998  dmrnssfld  5112  preddowncl  5426  nfunv  5632  opelf  5762  fvimacnv  6012  ffvelrn  6035  fnsnb  6098  f1imass  6180  onminex  6648  extmptsuppeq  6950  suppssr  6957  dftpos3  7002  wfrlem16  7062  oa00  7271  omordi  7278  omlimcl  7290  omeulem1  7294  nnmordi  7343  mapsn  7524  ixpf  7555  pw2f1olem  7685  pssnn  7799  findcard3  7823  ixpfi2  7881  fissuni  7888  elfiun  7953  dffi3  7954  ordiso2  8039  ordtypelem7  8048  ixpiunwdom  8115  inf3lem2  8143  cantnfp1lem3  8193  cantnfp1  8194  cantnflem1  8202  cantnf  8206  trcl  8220  r1ordg  8257  rankelb  8303  rankuni2b  8332  rankval4  8346  tcrank  8363  cplem1  8368  carduniima  8534  alephfp  8546  kmlem2  8588  isf32lem3  8792  domtriomlem  8879  axdc3lem2  8888  ac6num  8916  zorn2lem7  8939  ttukeylem6  8951  iundom2g  8972  fpwwe2lem13  9074  tskss  9190  tskr1om2  9200  inatsk  9210  gruss  9228  gruel  9235  grur1  9252  prlem934  9465  ltexprlem7  9474  supsr  9543  dedekind  9804  supadd  10582  supmullem2  10585  uzind  11034  iccsplit  11772  elfz0add  11898  elfz0addOLD  11899  predfz  11921  fsuppmapnn0fiub  12209  ccatval2  12727  swrdswrd  12818  swrdccatin12lem2a  12843  swrdccatin2  12845  swrdccatin12lem2c  12846  swrdccatin12  12849  sqrlem6  13311  isercolllem2  13728  fsumcvg  13777  isumrpcl  13900  fprodcvg  13983  rpnnen2lem4  14269  fproddvdsd  14369  saddisj  14438  sadass  14444  bitsshft  14448  smuval2  14455  smupvallem  14456  smu01lem  14458  smueqlem  14463  reumodprminv  14754  ramub1lem1  14983  firest  15330  mrissmrid  15546  initoeu2lem0  15907  acsfiindd  16422  acsmapd  16423  dirge  16482  issubmnd  16563  issubg2  16831  eqgid  16868  dprdff  17644  dprddisj2  17671  ablfac1c  17703  subrgdvds  18021  issubrg2  18027  lssssr  18175  lssats2  18222  lbspss  18304  lsmelval2  18307  lspprat  18375  lbsextlem2  18381  lbsextlem3  18382  lpigen  18479  mplcoe5lem  18690  psgndiflemB  19166  lsmcss  19253  obselocv  19289  f1lindf  19378  mdetdiaglem  19621  cpmadugsumlemF  19898  unitgOLD  19981  elcls  20087  clsndisj  20089  elcls3  20097  neindisj  20131  lpval  20153  lpsscls  20155  lpss3  20158  maxlp  20161  restntr  20196  ordtbas2  20205  ordtbas  20206  pnfnei  20234  mnfnei  20235  cncls2  20287  lmcnp  20318  lpcls  20378  hauscmplem  20419  2ndcdisj  20469  kgen2ss  20568  txuni2  20578  ptpjpre1  20584  tx1cn  20622  tx2cn  20623  prdstopn  20641  txlm  20661  imasnopn  20703  imasncld  20704  imasncls  20705  tgqtop  20725  regr1lem  20752  fgss2  20887  uzfbas  20911  ufilmax  20920  uffix2  20937  ufildr  20944  fmfnfmlem1  20967  fmco  20974  flimrest  20996  fclsopn  21027  fclscf  21038  flimfcls  21039  alexsubALTlem4  21063  qustgplem  21133  imasf1oxms  21502  prdsbl  21504  metrest  21537  iccntr  21837  reconnlem2  21843  caucfil  22251  caussi  22265  bcthlem5  22294  ovoliunlem1  22453  shft2rab  22459  sca2rab  22463  ovolicc2  22474  vitalilem2  22565  vitalilem5  22568  mbfinf  22619  mbfinfOLD  22620  i1f1lem  22645  mbfi1fseqlem4  22674  itgss  22767  itgcn  22798  c1liplem1  22946  c1lip1  22947  c1lip3  22949  ply1remlem  23111  plyexmo  23264  lgamucov  23961  fsumvma  24139  logfaclbnd  24148  axlowdimlem16  24985  axcontlem9  25000  wwlknred  25449  wwlknext  25450  clwlkswlks  25484  clwwlkf  25520  wwlksubclwwlk  25530  nbhashuvtx  25642  eupath2  25706  extwwlkfablem2  25804  subgoablo  26037  sspmval  26370  sspival  26375  sspimsval  26377  sspph  26494  ubthlem1  26510  shsubcl  26871  shorth  26946  elspansn3  27223  elnlfn  27579  elpjrn  27841  sumdmdlem2  28070  fimarab  28246  supssd  28292  infssd  28293  xrofsup  28359  cmpcref  28685  cntmeas  29056  1stmbfm  29090  2ndmbfm  29091  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemodife  29338  ballotlemimin  29346  ballotlemiminOLD  29384  bnj142OLD  29542  bnj1171  29817  bnj1280  29837  mrsubrn  30159  elfzm12  30327  trpredtr  30478  trpredmintr  30479  dftrpred3g  30481  trpredrec  30486  sltres  30558  nodenselem8  30582  ontgval  31096  poimirlem16  31920  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  itg2addnclem  31957  itg2addnclem2  31958  ftc1anclem7  31987  ismtyima  32099  lshpkr  32652  psubatN  33289  elpaddn0  33334  pclfinN  33434  diael  34580  dia2dimlem12  34612  dicelval1stN  34725  dicelval2nd  34726  dib2dim  34780  dih2dimbALTN  34782  dihlspsnssN  34869  dvh1dim  34979  lcfrvalsnN  35078  mapdrvallem2  35182  mapdpglem2  35210  hdmap10lem  35379  hdmap11lem2  35382  hdmapoc  35471  isnacs3  35521  aomclem2  35883  kelac1  35891  rngunsnply  36009  intabssd  36186  iunrelexp0  36264  dvconstbi  36653  expgrowth  36654  climsuselem1  37626  climsuse  37627  limcresiooub  37663  iblsplit  37783  iblspltprt  37790  stoweidlem62  37863  stoweidlem62OLD  37864  stirlinglem11  37886  fourierdlem41  37951  sge0fodjrnlem  38166  fafvelrn  38542  smonoord  38588  iccpartiltu  38606  iccpartigtl  38607  iccpartiun  38618  iccpartdisj  38621  bgoldbtbndlem2  38771  pfxccatin12  38836  pfxccatpfx2  38839  edgumgra  39042  umgredg  39077  subgreldmiedg  39128  umgrres1  39148  uhgraedgrnv  39282  c0rnghm  39532  lidldomn1  39540  lidlmmgm  39544  lidlmsgrp  39545  lidlrng  39546  rnghmsscmap  39595  rngcsect  39601  funcrngcsetc  39619  rhmsscmap  39641  rhmsscrnghm  39647  ringcsect  39652  funcringcsetc  39656  funcringcsetcALTV2lem9  39665  rhmsubclem4  39710  rhmsubcALTVlem4  39729  lincresunit3lem1  39893