Theorem sseld 3350

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 3345	. 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 1756   C_ wss 3323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337

This theorem is referenced by:  sselda  3351  sseldd  3352  ssneld  3353  elelpwi  3866  ssbrd  4328  uniopel  4590  exopxfr2  4979  dmrnssfld  5093  nfunv  5444  opelf  5569  fvimacnv  5813  suppssrOLD  5832  ffvelrn  5836  fnsnb  5893  f1imass  5972  onminex  6413  extmptsuppeq  6708  suppssr  6715  dftpos3  6758  oa00  6990  omordi  6997  omlimcl  7009  omeulem1  7013  nnmordi  7062  mapsn  7246  ixpf  7277  pw2f1olem  7407  pssnn  7523  findcard3  7547  ixpfi2  7601  fissuni  7608  elfiun  7672  dffi3  7673  ordiso2  7721  ordtypelem7  7730  ixpiunwdom  7798  sucprcregOLD  7807  inf3lem2  7827  cantnfp1lem3  7880  cantnfp1  7881  cantnflem1  7889  cantnf  7893  cantnfp1lem3OLD  7906  cantnfp1OLD  7907  cantnflem1OLD  7912  cantnfOLD  7915  trcl  7940  r1ordg  7977  rankelb  8023  rankuni2b  8052  rankval4  8066  tcrank  8083  cplem1  8088  carduniima  8258  alephfp  8270  kmlem2  8312  isf32lem3  8516  domtriomlem  8603  axdc3lem2  8612  ac6num  8640  zorn2lem7  8663  ttukeylem6  8675  iundom2g  8696  fpwwe2lem13  8801  tskss  8917  tskr1om2  8927  inatsk  8937  gruss  8955  gruel  8962  grur1  8979  prlem934  9194  ltexprlem7  9203  supsr  9271  dedekind  9525  supmullem2  10289  uzind  10725  iccsplit  11410  elfzelfzadd  11500  fzm1  11532  ccatval2  12269  swrdswrd  12346  swrdccatin12lem2a  12368  swrdccatin2  12370  swrdccatin12lem2c  12371  swrdccatin12  12374  sqrlem6  12729  isercolllem2  13135  fsumcvg  13181  isumrpcl  13298  rpnnen2lem4  13492  saddisj  13653  sadass  13659  bitsshft  13663  smuval2  13670  smupvallem  13671  smu01lem  13673  smueqlem  13678  reumodprminv  13864  ramub1lem1  14079  firest  14363  mrissmrid  14571  acsfiindd  15339  acsmapd  15340  dirge  15399  issubmnd  15441  issubg2  15687  eqgid  15724  dprdff  16484  dprdffOLD  16490  dprddisj2  16525  dprddisj2OLD  16526  ablfac1c  16560  subrgdvds  16857  issubrg2  16863  lssssr  17011  lssats2  17058  lbspss  17140  lsmelval2  17143  lspprat  17211  lbsextlem2  17217  lbsextlem3  17218  lpigen  17315  psgndiflemB  18005  lsmcss  18092  obselocv  18128  f1lindf  18226  mdet1  18383  unitg  18547  elcls  18652  clsndisj  18654  elcls3  18662  neindisj  18696  lpval  18718  lpsscls  18720  lpss3  18723  maxlp  18726  restntr  18761  ordtbas2  18770  ordtbas  18771  pnfnei  18799  mnfnei  18800  cncls2  18852  lmcnp  18883  lpcls  18943  hauscmplem  18984  2ndcdisj  19035  kgen2ss  19103  txuni2  19113  ptpjpre1  19119  tx1cn  19157  tx2cn  19158  prdstopn  19176  txlm  19196  imasnopn  19238  imasncld  19239  imasncls  19240  tgqtop  19260  regr1lem  19287  fgss2  19422  uzfbas  19446  ufilmax  19455  uffix2  19472  ufildr  19479  fmfnfmlem1  19502  fmco  19509  flimrest  19531  fclsopn  19562  fclscf  19573  flimfcls  19574  alexsubALTlem4  19597  divstgplem  19666  imasf1oxms  20039  prdsbl  20041  metrest  20074  iccntr  20373  reconnlem2  20379  caucfil  20769  caussi  20783  bcthlem5  20814  ovoliunlem1  20960  shft2rab  20966  sca2rab  20970  ovolicc2  20980  vitalilem2  21064  vitalilem5  21067  mbfinf  21118  i1f1lem  21142  mbfi1fseqlem4  21171  itgss  21264  itgcn  21295  c1liplem1  21443  c1lip1  21444  c1lip3  21446  ply1remlem  21609  plyexmo  21754  fsumvma  22527  logfaclbnd  22536  axlowdimlem16  23154  axcontlem9  23169  eupath2  23552  subgoablo  23749  sspmval  24082  sspival  24087  sspimsval  24089  sspph  24206  ubthlem1  24222  shsubcl  24574  shorth  24649  elspansn3  24926  elnlfn  25283  elpjrn  25545  sumdmdlem2  25774  supssd  25955  xrofsup  26006  cntmeas  26592  1stmbfm  26627  2ndmbfm  26628  sitgclbn  26681  ballotlemfc0  26827  ballotlemfcc  26828  ballotlemodife  26832  ballotlemimin  26840  lgamucov  26976  elfzm12  27271  fprodcvg  27394  preddowncl  27608  predfz  27615  trpredtr  27645  trpredmintr  27646  dftrpred3g  27648  trpredrec  27653  wfrlem16  27690  sltres  27756  nodenselem8  27780  ontgval  28229  supadd  28371  itg2addnclem  28396  itg2addnclem2  28397  ftc1anclem7  28426  ismtyima  28655  isnacs3  28999  aomclem2  29361  kelac1  29369  rngunsnply  29483  dvconstbi  29561  expgrowth  29562  climsuselem1  29733  climsuse  29734  stoweidlem62  29810  stirlinglem11  29832  fafvelrn  30029  uhgraedgrnv  30226  wwlknred  30308  wwlknext  30309  clwlkswlks  30376  clwwlkf  30409  wwlksubclwwlk  30419  nbhashuvtx  30487  extwwlkfablem2  30624  fsuppmapnn0fiub  30748  mdetdiaglem  30824  lincresunit3lem1  30902  bnj142OLD  31604  bnj1171  31878  bnj1280  31898  lshpkr  32602  psubatN  33239  elpaddn0  33284  pclfinN  33384  diael  34528  dia2dimlem12  34560  dicelval1stN  34673  dicelval2nd  34674  dib2dim  34728  dih2dimbALTN  34730  dihlspsnssN  34817  dvh1dim  34927  lcfrvalsnN  35026  mapdrvallem2  35130  mapdpglem2  35158  hdmap10lem  35327  hdmap11lem2  35330  hdmapoc  35419