Theorem sseld 3307

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 3302	. 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 1721   C_ wss 3280

This theorem is referenced by:  sselda  3308  sseldd  3309  ssneld  3310  elelpwi  3769  ssbrd  4213  uniopel  4420  onminex  4746  dmrnssfld  5088  nfunv  5443  opelf  5565  fvimacnv  5804  suppssr  5823  ffvelrn  5827  f1imass  5969  exopxfr2  6370  dftpos3  6456  oa00  6761  omordi  6768  omlimcl  6780  omeulem1  6784  nnmordi  6833  mapsn  7014  ixpf  7043  pw2f1olem  7171  pssnn  7286  findcard3  7309  ixpfi2  7363  fissuni  7369  elfiun  7393  dffi3  7394  ordiso2  7440  ordtypelem7  7449  ixpiunwdom  7515  sucprcreg  7523  inf3lem2  7540  cantnfreslem  7587  cantnfp1lem3  7592  cantnfp1  7593  cantnflem1  7601  cantnf  7605  trcl  7620  r1ordg  7660  rankelb  7706  rankuni2b  7735  rankval4  7749  tcrank  7764  cplem1  7769  carduniima  7933  alephfp  7945  kmlem2  7987  isf32lem3  8191  domtriomlem  8278  axdc3lem2  8287  ac6num  8315  zorn2lem7  8338  ttukeylem6  8350  iundom2g  8371  fpwwe2lem13  8473  tskss  8589  tskr1om2  8599  inatsk  8609  gruss  8627  gruel  8634  grur1  8651  prlem934  8866  ltexprlem7  8875  supsr  8943  supmullem2  9931  uzind  10317  iccsplit  10985  fzm1  11082  ccatval2  11701  sqrlem6  12008  isercolllem2  12414  fsumcvg  12461  isumrpcl  12578  rpnnen2lem4  12772  saddisj  12932  sadass  12938  bitsshft  12942  smuval2  12949  smupvallem  12950  smu01lem  12952  smueqlem  12957  ramub1lem1  13349  firest  13615  mrissmrid  13821  acsfiindd  14558  acsmapd  14559  dirge  14637  issubmnd  14679  issubg2  14914  eqgid  14947  dprdff  15525  dprddisj2  15552  ablfac1c  15584  subrgdvds  15837  issubrg2  15843  lssssr  15984  lssats2  16031  lbspss  16109  lsmelval2  16112  lspprat  16180  lbsextlem2  16186  lbsextlem3  16187  lpigen  16282  lsmcss  16874  obselocv  16910  unitg  16987  elcls  17092  clsndisj  17094  elcls3  17102  neindisj  17136  lpval  17158  lpsscls  17160  lpss3  17163  maxlp  17165  restntr  17200  ordtbas2  17209  ordtbas  17210  pnfnei  17238  mnfnei  17239  cncls2  17291  lmcnp  17322  lpcls  17382  hauscmplem  17423  2ndcdisj  17472  kgen2ss  17540  txuni2  17550  ptpjpre1  17556  tx1cn  17594  tx2cn  17595  prdstopn  17613  txlm  17633  imasnopn  17675  imasncld  17676  imasncls  17677  tgqtop  17697  regr1lem  17724  fgss2  17859  uzfbas  17883  ufilmax  17892  uffix2  17909  ufildr  17916  fmfnfmlem1  17939  fmco  17946  flimrest  17968  fclsopn  17999  fclscf  18010  flimfcls  18011  alexsubALTlem4  18034  divstgplem  18103  imasf1oxms  18472  prdsbl  18474  metrest  18507  iccntr  18805  reconnlem2  18811  caucfil  19189  caussi  19203  bcthlem5  19234  ovoliunlem1  19351  shft2rab  19357  sca2rab  19361  ovolicc2  19371  vitalilem2  19454  vitalilem5  19457  mbfinf  19510  i1f1lem  19534  mbfi1fseqlem4  19563  itgss  19656  itgcn  19687  c1liplem1  19833  c1lip1  19834  c1lip3  19836  ply1remlem  20038  plyexmo  20183  fsumvma  20950  logfaclbnd  20959  eupath2  21655  subgoablo  21852  sspmval  22185  sspival  22190  sspimsval  22192  sspph  22309  ubthlem1  22325  shsubcl  22676  shorth  22750  elspansn3  23027  elnlfn  23384  elpjrn  23646  sumdmdlem2  23875  supssd  24051  xrofsup  24079  cntmeas  24533  1stmbfm  24563  2ndmbfm  24564  sitgclbn  24610  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemodife  24708  ballotlemimin  24716  lgamucov  24775  elfzm12  25065  dedekind  25140  fprodcvg  25209  preddowncl  25410  predfz  25417  trpredtr  25447  trpredmintr  25448  dftrpred3g  25450  trpredrec  25455  wfrlem16  25485  sltres  25532  nodenselem8  25556  axlowdimlem16  25800  axcontlem9  25815  ontgval  26085  supadd  26138  itg2addnclem  26155  itg2addnclem2  26156  ismtyima  26402  isnacs3  26654  aomclem2  27020  kelac1  27029  f1lindf  27160  rngunsnply  27246  dvconstbi  27419  expgrowth  27420  climsuselem1  27600  climsuse  27601  stoweidlem62  27678  stirlinglem11  27700  fafvelrn  27901  elfzelfzadd  27982  swrdswrd  28011  swrdccatin2  28018  swrdccatin12lem3a  28021  swrdccatin12lem3c  28023  swrdccatin12lem4  28025  swrdccatin12  28026  uhgraedgrnv  28032  bnj142  28799  bnj1171  29075  bnj1280  29095  lshpkr  29600  psubatN  30237  elpaddn0  30282  pclfinN  30382  diael  31526  dia2dimlem12  31558  dicelval1stN  31671  dicelval2nd  31672  dib2dim  31726  dih2dimbALTN  31728  dihlspsnssN  31815  dvh1dim  31925  lcfrvalsnN  32024  mapdrvallem2  32128  mapdpglem2  32156  hdmap10lem  32325  hdmap11lem2  32328  hdmapoc  32417

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294