Theorem sselda 3179

Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)

Hypothesis

Ref	Expression
sseld.1	|- ( ph -> A C_ B )

Assertion

Ref	Expression
sselda	|- ( ( ph /\ C e. A ) -> C e. B )

Proof of Theorem sselda

Step	Hyp	Ref	Expression
1		sseld.1	. . 3 |- ( ph -> A C_ B )
2	1	sseld 3178	. 2 |- ( ph -> ( C e. A -> C e. B ) )
3	2	imp 124	1 |- ( ( ph /\ C e. A ) -> C e. B )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2164   C_ wss 3153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  pwntru  4228  elrel  4761  ffvresb  5721  1stdm  6235  tfrlem1  6361  tfrlemiubacc  6383  tfr1onlemubacc  6399  tfrcllemubacc  6412  erinxp  6663  fundmen  6860  supisolem  7067  ordiso2  7094  difinfsn  7159  ctssdc  7172  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  pw1on  7286  elprnql  7541  elprnqu  7542  suplocexprlemml  7776  axpre-suploclemres  7961  suprleubex  8973  un0addcl  9273  un0mulcl  9274  suprzclex  9415  supminfex  9662  infregelbex  9663  icoshftf1o  10057  elfzom1elfzo  10270  zpnn0elfzo  10274  seqfveqg  10549  seq3fveq  10550  monoord2  10557  seqsplitg  10560  seqcaopr2g  10565  seqf1oglem2a  10589  seqf1oglem2  10591  seqhomog  10601  seq3coll  10913  rexanre  11364  rexico  11365  summodclem2a  11524  isumss  11534  fisumss  11535  fsum3cvg3  11539  fsumsplit  11550  fsum2dlemstep  11577  fisum0diag2  11590  fsumlessfi  11603  fsumabs  11608  telfsumo  11609  fsumparts  11613  fsumrelem  11614  fsumiun  11620  hashuni  11625  binom1dif  11630  isumsplit  11634  isumrpcl  11637  isumlessdc  11639  mertenslemi1  11678  clim2prod  11682  prodfrecap  11689  prodmodclem2a  11719  prodssdc  11732  fprodssdc  11733  fprodsplitdc  11739  fprod2dlemstep  11765  4sqlemffi  12534  4sqleminfi  12535  4sqlem11  12539  ennnfonelemfun  12574  ennnfonelemf1  12575  restid2  12859  gsumress  12978  gsumsplit1r  12981  issubmnd  13023  ress0g  13024  grpinvssd  13149  subginv  13251  issubg2m  13259  issubg4m  13263  subgintm  13268  ssnmz  13281  resghm  13330  conjnmz  13349  conjnmzb  13350  subcmnd  13403  ringidss  13525  invrpropdg  13645  subrg1  13727  subrginv  13733  subrgunit  13735  islss3  13875  lssintclm  13880  tgclb  14233  tgidm  14242  tgrest  14337  txcnp  14439  txdis1cn  14446  psmetres2  14501  blpnfctr  14607  xmetresbl  14608  mopni2  14651  mopni3  14652  rnblopn  14657  xmettx  14678  tgioo  14714  fsumcncntop  14724  climcncf  14739  suplociccreex  14778  suplociccex  14779  dedekindicc  14787  ivthdec  14798  dvfgg  14842  dvcnp2cntop  14848  dvaddxxbr  14850  dvcjbr  14857  gausslemma2dlem2  15178  gausslemma2dlem3  15179  pwtrufal  15488