Theorem sseld 3466

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 3461	. 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 1758   C_ wss 3439

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453

This theorem is referenced by:  sselda  3467  sseldd  3468  ssneld  3469  elelpwi  3982  ssbrd  4444  uniopel  4706  exopxfr2  5095  dmrnssfld  5209  nfunv  5560  opelf  5685  fvimacnv  5930  suppssrOLD  5949  ffvelrn  5953  fnsnb  6010  f1imass  6089  onminex  6531  extmptsuppeq  6826  suppssr  6833  dftpos3  6876  oa00  7111  omordi  7118  omlimcl  7130  omeulem1  7134  nnmordi  7183  mapsn  7367  ixpf  7398  pw2f1olem  7528  pssnn  7645  findcard3  7669  ixpfi2  7723  fissuni  7730  elfiun  7794  dffi3  7795  ordiso2  7843  ordtypelem7  7852  ixpiunwdom  7920  sucprcregOLD  7929  inf3lem2  7949  cantnfp1lem3  8002  cantnfp1  8003  cantnflem1  8011  cantnf  8015  cantnfp1lem3OLD  8028  cantnfp1OLD  8029  cantnflem1OLD  8034  cantnfOLD  8037  trcl  8062  r1ordg  8099  rankelb  8145  rankuni2b  8174  rankval4  8188  tcrank  8205  cplem1  8210  carduniima  8380  alephfp  8392  kmlem2  8434  isf32lem3  8638  domtriomlem  8725  axdc3lem2  8734  ac6num  8762  zorn2lem7  8785  ttukeylem6  8797  iundom2g  8818  fpwwe2lem13  8923  tskss  9039  tskr1om2  9049  inatsk  9059  gruss  9077  gruel  9084  grur1  9101  prlem934  9316  ltexprlem7  9325  supsr  9393  dedekind  9647  supmullem2  10411  uzind  10847  iccsplit  11538  elfzelfzadd  11628  fzm1  11660  ccatval2  12398  swrdswrd  12475  swrdccatin12lem2a  12497  swrdccatin2  12499  swrdccatin12lem2c  12500  swrdccatin12  12503  sqrlem6  12858  isercolllem2  13264  fsumcvg  13310  isumrpcl  13427  rpnnen2lem4  13621  saddisj  13782  sadass  13788  bitsshft  13792  smuval2  13799  smupvallem  13800  smu01lem  13802  smueqlem  13807  reumodprminv  13993  ramub1lem1  14208  firest  14493  mrissmrid  14701  acsfiindd  15469  acsmapd  15470  dirge  15529  issubmnd  15571  issubg2  15818  eqgid  15855  dprdff  16621  dprdffOLD  16627  dprddisj2  16662  dprddisj2OLD  16663  ablfac1c  16697  subrgdvds  17005  issubrg2  17011  lssssr  17160  lssats2  17207  lbspss  17289  lsmelval2  17292  lspprat  17360  lbsextlem2  17366  lbsextlem3  17367  lpigen  17464  mplcoe5lem  17674  psgndiflemB  18158  lsmcss  18245  obselocv  18281  f1lindf  18379  mdetdiaglem  18539  unitg  18707  elcls  18812  clsndisj  18814  elcls3  18822  neindisj  18856  lpval  18878  lpsscls  18880  lpss3  18883  maxlp  18886  restntr  18921  ordtbas2  18930  ordtbas  18931  pnfnei  18959  mnfnei  18960  cncls2  19012  lmcnp  19043  lpcls  19103  hauscmplem  19144  2ndcdisj  19195  kgen2ss  19263  txuni2  19273  ptpjpre1  19279  tx1cn  19317  tx2cn  19318  prdstopn  19336  txlm  19356  imasnopn  19398  imasncld  19399  imasncls  19400  tgqtop  19420  regr1lem  19447  fgss2  19582  uzfbas  19606  ufilmax  19615  uffix2  19632  ufildr  19639  fmfnfmlem1  19662  fmco  19669  flimrest  19691  fclsopn  19722  fclscf  19733  flimfcls  19734  alexsubALTlem4  19757  divstgplem  19826  imasf1oxms  20199  prdsbl  20201  metrest  20234  iccntr  20533  reconnlem2  20539  caucfil  20929  caussi  20943  bcthlem5  20974  ovoliunlem1  21120  shft2rab  21126  sca2rab  21130  ovolicc2  21140  vitalilem2  21225  vitalilem5  21228  mbfinf  21279  i1f1lem  21303  mbfi1fseqlem4  21332  itgss  21425  itgcn  21456  c1liplem1  21604  c1lip1  21605  c1lip3  21607  ply1remlem  21770  plyexmo  21915  fsumvma  22688  logfaclbnd  22697  axlowdimlem16  23375  axcontlem9  23390  eupath2  23773  subgoablo  23970  sspmval  24303  sspival  24308  sspimsval  24310  sspph  24427  ubthlem1  24443  shsubcl  24795  shorth  24870  elspansn3  25147  elnlfn  25504  elpjrn  25766  sumdmdlem2  25995  supssd  26175  xrofsup  26226  cntmeas  26805  1stmbfm  26839  2ndmbfm  26840  sitgclbn  26893  ballotlemfc0  27039  ballotlemfcc  27040  ballotlemodife  27044  ballotlemimin  27052  lgamucov  27188  elfzm12  27484  fprodcvg  27607  preddowncl  27821  predfz  27828  trpredtr  27858  trpredmintr  27859  dftrpred3g  27861  trpredrec  27866  wfrlem16  27903  sltres  27969  nodenselem8  27993  ontgval  28441  supadd  28586  itg2addnclem  28611  itg2addnclem2  28612  ftc1anclem7  28641  ismtyima  28870  isnacs3  29214  aomclem2  29576  kelac1  29584  rngunsnply  29698  dvconstbi  29776  expgrowth  29777  climsuselem1  29948  climsuse  29949  stoweidlem62  30025  stirlinglem11  30047  fafvelrn  30244  uhgraedgrnv  30441  wwlknred  30523  wwlknext  30524  clwlkswlks  30591  clwwlkf  30624  wwlksubclwwlk  30634  nbhashuvtx  30702  extwwlkfablem2  30839  fsuppmapnn0fiub  30967  lincresunit3lem1  31165  cpmadugsumlemF  31382  bnj142OLD  32069  bnj1171  32343  bnj1280  32363  lshpkr  33120  psubatN  33757  elpaddn0  33802  pclfinN  33902  diael  35046  dia2dimlem12  35078  dicelval1stN  35191  dicelval2nd  35192  dib2dim  35246  dih2dimbALTN  35248  dihlspsnssN  35335  dvh1dim  35445  lcfrvalsnN  35544  mapdrvallem2  35648  mapdpglem2  35676  hdmap10lem  35845  hdmap11lem2  35848  hdmapoc  35937