Theorem sseld 3343

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 3338	. 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 1755   C_ wss 3316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330

This theorem is referenced by:  sselda  3344  sseldd  3345  ssneld  3346  elelpwi  3859  ssbrd  4321  uniopel  4583  exopxfr2  4971  dmrnssfld  5085  nfunv  5437  opelf  5562  fvimacnv  5806  suppssrOLD  5825  ffvelrn  5829  fnsnb  5885  f1imass  5964  onminex  6407  extmptsuppeq  6702  suppssr  6709  dftpos3  6752  oa00  6986  omordi  6993  omlimcl  7005  omeulem1  7009  nnmordi  7058  mapsn  7242  ixpf  7273  pw2f1olem  7403  pssnn  7519  findcard3  7543  ixpfi2  7597  fissuni  7604  elfiun  7668  dffi3  7669  ordiso2  7717  ordtypelem7  7726  ixpiunwdom  7794  sucprcregOLD  7803  inf3lem2  7823  cantnfp1lem3  7876  cantnfp1  7877  cantnflem1  7885  cantnf  7889  cantnfp1lem3OLD  7902  cantnfp1OLD  7903  cantnflem1OLD  7908  cantnfOLD  7911  trcl  7936  r1ordg  7973  rankelb  8019  rankuni2b  8048  rankval4  8062  tcrank  8079  cplem1  8084  carduniima  8254  alephfp  8266  kmlem2  8308  isf32lem3  8512  domtriomlem  8599  axdc3lem2  8608  ac6num  8636  zorn2lem7  8659  ttukeylem6  8671  iundom2g  8692  fpwwe2lem13  8797  tskss  8913  tskr1om2  8923  inatsk  8933  gruss  8951  gruel  8958  grur1  8975  prlem934  9190  ltexprlem7  9199  supsr  9267  dedekind  9521  supmullem2  10285  uzind  10721  iccsplit  11405  elfzelfzadd  11493  fzm1  11524  ccatval2  12261  swrdswrd  12338  swrdccatin12lem2a  12360  swrdccatin2  12362  swrdccatin12lem2c  12363  swrdccatin12  12366  sqrlem6  12721  isercolllem2  13127  fsumcvg  13173  isumrpcl  13289  rpnnen2lem4  13483  saddisj  13644  sadass  13650  bitsshft  13654  smuval2  13661  smupvallem  13662  smu01lem  13664  smueqlem  13669  reumodprminv  13855  ramub1lem1  14070  firest  14354  mrissmrid  14562  acsfiindd  15330  acsmapd  15331  dirge  15390  issubmnd  15432  issubg2  15676  eqgid  15713  dprdff  16470  dprdffOLD  16476  dprddisj2  16511  dprddisj2OLD  16512  ablfac1c  16546  subrgdvds  16803  issubrg2  16809  lssssr  16956  lssats2  17003  lbspss  17085  lsmelval2  17088  lspprat  17156  lbsextlem2  17162  lbsextlem3  17163  lpigen  17260  psgndiflemB  17872  lsmcss  17959  obselocv  17995  f1lindf  18093  mdet1  18250  unitg  18414  elcls  18519  clsndisj  18521  elcls3  18529  neindisj  18563  lpval  18585  lpsscls  18587  lpss3  18590  maxlp  18593  restntr  18628  ordtbas2  18637  ordtbas  18638  pnfnei  18666  mnfnei  18667  cncls2  18719  lmcnp  18750  lpcls  18810  hauscmplem  18851  2ndcdisj  18902  kgen2ss  18970  txuni2  18980  ptpjpre1  18986  tx1cn  19024  tx2cn  19025  prdstopn  19043  txlm  19063  imasnopn  19105  imasncld  19106  imasncls  19107  tgqtop  19127  regr1lem  19154  fgss2  19289  uzfbas  19313  ufilmax  19322  uffix2  19339  ufildr  19346  fmfnfmlem1  19369  fmco  19376  flimrest  19398  fclsopn  19429  fclscf  19440  flimfcls  19441  alexsubALTlem4  19464  divstgplem  19533  imasf1oxms  19906  prdsbl  19908  metrest  19941  iccntr  20240  reconnlem2  20246  caucfil  20636  caussi  20650  bcthlem5  20681  ovoliunlem1  20827  shft2rab  20833  sca2rab  20837  ovolicc2  20847  vitalilem2  20931  vitalilem5  20934  mbfinf  20985  i1f1lem  21009  mbfi1fseqlem4  21038  itgss  21131  itgcn  21162  c1liplem1  21310  c1lip1  21311  c1lip3  21313  ply1remlem  21519  plyexmo  21664  fsumvma  22437  logfaclbnd  22446  axlowdimlem16  23026  axcontlem9  23041  eupath2  23424  subgoablo  23621  sspmval  23954  sspival  23959  sspimsval  23961  sspph  24078  ubthlem1  24094  shsubcl  24446  shorth  24521  elspansn3  24798  elnlfn  25155  elpjrn  25417  sumdmdlem2  25646  supssd  25828  xrofsup  25878  cntmeas  26494  1stmbfm  26529  2ndmbfm  26530  sitgclbn  26577  ballotlemfc0  26723  ballotlemfcc  26724  ballotlemodife  26728  ballotlemimin  26736  lgamucov  26872  elfzm12  27167  fprodcvg  27290  preddowncl  27504  predfz  27511  trpredtr  27541  trpredmintr  27542  dftrpred3g  27544  trpredrec  27549  wfrlem16  27586  sltres  27652  nodenselem8  27676  ontgval  28125  supadd  28262  itg2addnclem  28287  itg2addnclem2  28288  ftc1anclem7  28317  ismtyima  28546  isnacs3  28891  aomclem2  29253  kelac1  29261  rngunsnply  29375  dvconstbi  29453  expgrowth  29454  climsuselem1  29626  climsuse  29627  stoweidlem62  29703  stirlinglem11  29725  fafvelrn  29922  uhgraedgrnv  30119  wwlknred  30201  wwlknext  30202  clwlkswlks  30269  clwwlkf  30302  wwlksubclwwlk  30312  nbhashuvtx  30380  extwwlkfablem2  30517  lincresunit3lem1  30722  bnj142OLD  31419  bnj1171  31693  bnj1280  31713  lshpkr  32335  psubatN  32972  elpaddn0  33017  pclfinN  33117  diael  34261  dia2dimlem12  34293  dicelval1stN  34406  dicelval2nd  34407  dib2dim  34461  dih2dimbALTN  34463  dihlspsnssN  34550  dvh1dim  34660  lcfrvalsnN  34759  mapdrvallem2  34863  mapdpglem2  34891  hdmap10lem  35060  hdmap11lem2  35063  hdmapoc  35152