Theorem sseld 3503

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 3498	. 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 1767   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490

This theorem is referenced by:  sselda  3504  sseldd  3505  ssneld  3506  elelpwi  4021  ssbrd  4488  uniopel  4751  exopxfr2  5146  dmrnssfld  5260  nfunv  5618  opelf  5746  fvimacnv  5995  suppssrOLD  6014  ffvelrn  6018  fnsnb  6079  f1imass  6159  onminex  6621  extmptsuppeq  6924  suppssr  6931  dftpos3  6973  oa00  7208  omordi  7215  omlimcl  7227  omeulem1  7231  nnmordi  7280  mapsn  7460  ixpf  7491  pw2f1olem  7621  pssnn  7738  findcard3  7762  ixpfi2  7817  fissuni  7824  elfiun  7889  dffi3  7890  ordiso2  7939  ordtypelem7  7948  ixpiunwdom  8016  sucprcregOLD  8025  inf3lem2  8045  cantnfp1lem3  8098  cantnfp1  8099  cantnflem1  8107  cantnf  8111  cantnfp1lem3OLD  8124  cantnfp1OLD  8125  cantnflem1OLD  8130  cantnfOLD  8133  trcl  8158  r1ordg  8195  rankelb  8241  rankuni2b  8270  rankval4  8284  tcrank  8301  cplem1  8306  carduniima  8476  alephfp  8488  kmlem2  8530  isf32lem3  8734  domtriomlem  8821  axdc3lem2  8830  ac6num  8858  zorn2lem7  8881  ttukeylem6  8893  iundom2g  8914  fpwwe2lem13  9019  tskss  9135  tskr1om2  9145  inatsk  9155  gruss  9173  gruel  9180  grur1  9197  prlem934  9410  ltexprlem7  9419  supsr  9488  dedekind  9742  supmullem2  10509  uzind  10951  iccsplit  11652  fzm1  11757  elfz0add  11773  fsuppmapnn0fiub  12064  ccatval2  12560  swrdswrd  12647  swrdccatin12lem2a  12672  swrdccatin2  12674  swrdccatin12lem2c  12675  swrdccatin12  12678  sqrlem6  13043  isercolllem2  13450  fsumcvg  13496  isumrpcl  13617  rpnnen2lem4  13811  saddisj  13973  sadass  13979  bitsshft  13983  smuval2  13990  smupvallem  13991  smu01lem  13993  smueqlem  13998  reumodprminv  14187  ramub1lem1  14402  firest  14687  mrissmrid  14895  acsfiindd  15663  acsmapd  15664  dirge  15723  issubmnd  15766  issubg2  16018  eqgid  16055  dprdff  16845  dprdffOLD  16851  dprddisj2  16886  dprddisj2OLD  16887  ablfac1c  16921  subrgdvds  17238  issubrg2  17244  lssssr  17394  lssats2  17441  lbspss  17523  lsmelval2  17526  lspprat  17594  lbsextlem2  17600  lbsextlem3  17601  lpigen  17698  mplcoe5lem  17917  psgndiflemB  18419  lsmcss  18506  obselocv  18542  f1lindf  18640  mdetdiaglem  18883  cpmadugsumlemF  19160  unitg  19251  elcls  19356  clsndisj  19358  elcls3  19366  neindisj  19400  lpval  19422  lpsscls  19424  lpss3  19427  maxlp  19430  restntr  19465  ordtbas2  19474  ordtbas  19475  pnfnei  19503  mnfnei  19504  cncls2  19556  lmcnp  19587  lpcls  19647  hauscmplem  19688  2ndcdisj  19739  kgen2ss  19807  txuni2  19817  ptpjpre1  19823  tx1cn  19861  tx2cn  19862  prdstopn  19880  txlm  19900  imasnopn  19942  imasncld  19943  imasncls  19944  tgqtop  19964  regr1lem  19991  fgss2  20126  uzfbas  20150  ufilmax  20159  uffix2  20176  ufildr  20183  fmfnfmlem1  20206  fmco  20213  flimrest  20235  fclsopn  20266  fclscf  20277  flimfcls  20278  alexsubALTlem4  20301  divstgplem  20370  imasf1oxms  20743  prdsbl  20745  metrest  20778  iccntr  21077  reconnlem2  21083  caucfil  21473  caussi  21487  bcthlem5  21518  ovoliunlem1  21664  shft2rab  21670  sca2rab  21674  ovolicc2  21684  vitalilem2  21769  vitalilem5  21772  mbfinf  21823  i1f1lem  21847  mbfi1fseqlem4  21876  itgss  21969  itgcn  22000  c1liplem1  22148  c1lip1  22149  c1lip3  22151  ply1remlem  22314  plyexmo  22459  fsumvma  23232  logfaclbnd  23241  axlowdimlem16  23952  axcontlem9  23967  wwlknred  24415  wwlknext  24416  clwlkswlks  24450  clwwlkf  24486  wwlksubclwwlk  24496  nbhashuvtx  24608  eupath2  24672  extwwlkfablem2  24771  subgoablo  25005  sspmval  25338  sspival  25343  sspimsval  25345  sspph  25462  ubthlem1  25478  shsubcl  25830  shorth  25905  elspansn3  26182  elnlfn  26539  elpjrn  26801  sumdmdlem2  27030  supssd  27215  xrofsup  27266  cntmeas  27853  1stmbfm  27887  2ndmbfm  27888  sitgclbn  27941  ballotlemfc0  28087  ballotlemfcc  28088  ballotlemodife  28092  ballotlemimin  28100  lgamucov  28236  elfzm12  28532  fprodcvg  28655  preddowncl  28869  predfz  28876  trpredtr  28906  trpredmintr  28907  dftrpred3g  28909  trpredrec  28914  wfrlem16  28951  sltres  29017  nodenselem8  29041  ontgval  29489  supadd  29635  itg2addnclem  29659  itg2addnclem2  29660  ftc1anclem7  29689  ismtyima  29918  isnacs3  30262  aomclem2  30621  kelac1  30629  rngunsnply  30743  dvconstbi  30855  expgrowth  30856  icoiccdif  31144  climsuselem1  31165  climsuse  31166  limciccioolb  31179  lptioo2  31189  limcicciooub  31195  limcresiooub  31200  cncfiooicclem1  31248  iblsplit  31300  iblspltprt  31307  itgsubsticclem  31309  itgsbtaddcnst  31316  stoweidlem62  31378  stirlinglem11  31400  fourierdlem1  31424  fourierdlem37  31460  fourierdlem41  31464  fourierdlem54  31477  fourierdlem79  31502  fourierdlem82  31505  fourierdlem93  31516  fafvelrn  31738  uhgraedgrnv  31832  lincresunit3lem1  32170  bnj142OLD  32870  bnj1171  33144  bnj1280  33164  lshpkr  33923  psubatN  34560  elpaddn0  34605  pclfinN  34705  diael  35849  dia2dimlem12  35881  dicelval1stN  35994  dicelval2nd  35995  dib2dim  36049  dih2dimbALTN  36051  dihlspsnssN  36138  dvh1dim  36248  lcfrvalsnN  36347  mapdrvallem2  36451  mapdpglem2  36479  hdmap10lem  36648  hdmap11lem2  36651  hdmapoc  36740