Theorem sseld 2619

Description: Membership deduction from subclass relationship.

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 2615	. 2 |- (A C_ B -> (C e. A -> C e. B))
3	1, 2	syl 12	1 |- (ph -> (C e. A -> C e. B))

Syntax hints:   -> wi 3   e. wcel 1300   C_ wss 2593

This theorem is referenced by:  sseldd 2620  elelpwi 3040  ssbrd 3378  uniopel 3556  elrel 4086  dmrnssfld 4205  nfunv 4453  opelf 4579  fvimacnv 4778  ffvelrn 4787  1stdm 5049  oa00 5241  omordi 5245  omlimcl 5257  mapsn 5404  ixpf 5415  uniixp 5416  pssnn 5628  ordtypelem6 5689  sucprcreg 5703  inf3lem2 5720  trcl 5752  r1ord 5766  rankwflem 5776  rankr1 5785  ssrankr1 5787  rankel 5791  r1pwcl 5798  rankuni2 5801  rankval4 5813  cplem1 5850  kmlem2 5928  zorn2lem7 5956  carduniima 6038  alephfp 6048  elprpq 6247  genpss 6259  ltexprlem7 6300  suprub 7265  uzind 7417  elfzp1 7683  fsequb 7702  fsequb2 7703  seqzfveq 7797  fsump1s 8273  fsumcllem 8274  fsum1ps 8278  fsumsplit 8280  fsumadd 8282  fsumcom 8288  fsumrev 8289  fsummulc1 8293  fsumcmp 8300  fsumcmpndx2 8302  fsumabs 8303  fsum0diaglem2 8519  fsum0diag2 8521  fsum0diag3 8522  fsum0diag4 8523  infxpidmlem5 8825  infxpidmlem7 8827  infxpidmlem8 8828  unitg 8893  tgss2 8907  elcls 8980  clsndisj 8982  elcls3 8987  neindisj 9007  lpval 9019  lpsscls 9021  clslp 9024  cncnpi 9050  cncnp 9055  opni2 9142  rnblopn 9151  caussi 9232  bcthlem28 9304  subgabl 9432  nmcn3 9680  nmcnc 9681  sspmval 9731  sspival 9736  sspimsval 9738  sspph 9856  ubthlem6 9877  tx1cn 10223  tx2cn 10224  subtopmetlem 10255  subtopmet 10256  fbfgss 10288  flimnei 10301  elfilmap2 10313  shel 10713  shsubcl 10722  shsubclOLD 10723  chel 10733  ocorth 10797  shorth 10801  shsel 10911  elspansn3 11128  elnlfn2 11490  sumdmdlem2 11991  bnj1140 12938  bnj1284 13482  bnj1280 13483  seqzresval2 13616  suprzcl 13658  preddowncl 13907  orderseqlem 13953  wfrlem16 13972  axdenselem8 14026  axfelem8 14038  axfelem9 14039  axfelem12 14042  axfelem15 14045  axfelem16 14046  axfelem17 14047  oprabex2gpop 14337  mappow 14413  fprodp1s 14682  fprodadd 14713  tpgprop1 14986  tpgprop2 14987  supnuf 15041  dmrngcmp 15098  dualcat2lem 15129  dualded2lem 15130  dualded 15132  dualcat2 15133  tarsuc3 15246  vtarsuelt 15272  partarelt2 15274  elfiun 15369  fictblem 15370  ordtypelem6OLD 15380  subntr 15425  cptclsscpt 15432  compfipin0lem 15435  alexsublem4 15440  alexsub 15441  reconnlem4 15449  reconnlem5 15450  iccconn 15453  neibastop2lem2 15520  fnejoin1 15530  fnejoin2 15531  uffixfr 15575  fmfnfmlem2 15595  fmfnfmlem4 15597  fmfnfm 15598  flimfbas 15601  isfclus 15606  fclusbas 15610  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscomp 15621  tailuni 15638  fimax 15746  fzm1 15796  lpss2 15842  mettrifi2 15848  geomcau 15849  iccsplit 15854  lincmb01icc 15879  lmtlm 15908  txmet 15925  sstotbnd 15936  totbndbnd 15944  ismtyhmeolem 15950  heiborlem1 15955  heiborlem15 15969  heiborlem16 15970  recms 16010  iccbnd 16026  pcoval1 16074  psubat 17235  elpaddn0 17261  osumcllem10 17373  pexmidlem7 17384

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain