Theorem sselda 3156

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 3155	. 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 2148   C_ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  pwntru  4200  elrel  4729  ffvresb  5680  1stdm  6183  tfrlem1  6309  tfrlemiubacc  6331  tfr1onlemubacc  6347  tfrcllemubacc  6360  erinxp  6609  fundmen  6806  supisolem  7007  ordiso2  7034  difinfsn  7099  ctssdc  7112  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  pw1on  7225  elprnql  7480  elprnqu  7481  suplocexprlemml  7715  axpre-suploclemres  7900  suprleubex  8911  un0addcl  9209  un0mulcl  9210  suprzclex  9351  supminfex  9597  infregelbex  9598  icoshftf1o  9991  elfzom1elfzo  10203  zpnn0elfzo  10207  seq3fveq  10471  monoord2  10477  seq3coll  10822  rexanre  11229  rexico  11230  summodclem2a  11389  isumss  11399  fisumss  11400  fsum3cvg3  11404  fsumsplit  11415  fsum2dlemstep  11442  fisum0diag2  11455  fsumlessfi  11468  fsumabs  11473  telfsumo  11474  fsumparts  11478  fsumrelem  11479  fsumiun  11485  hashuni  11490  binom1dif  11495  isumsplit  11499  isumrpcl  11502  isumlessdc  11504  mertenslemi1  11543  clim2prod  11547  prodfrecap  11554  prodmodclem2a  11584  prodssdc  11597  fprodssdc  11598  fprodsplitdc  11604  fprod2dlemstep  11630  ennnfonelemfun  12418  ennnfonelemf1  12419  restid2  12697  issubmnd  12843  ress0g  12844  grpinvssd  12947  subginv  13041  issubg2m  13049  issubg4m  13053  subgintm  13058  ssnmz  13071  subcmnd  13129  ringidss  13212  invrpropdg  13318  subrg1  13352  subrginv  13358  subrgunit  13360  tgclb  13568  tgidm  13577  tgrest  13672  txcnp  13774  txdis1cn  13781  psmetres2  13836  blpnfctr  13942  xmetresbl  13943  mopni2  13986  mopni3  13987  rnblopn  13992  xmettx  14013  tgioo  14049  fsumcncntop  14059  climcncf  14074  suplociccreex  14105  suplociccex  14106  dedekindicc  14114  ivthdec  14125  dvfgg  14160  dvcnp2cntop  14166  dvaddxxbr  14168  dvcjbr  14175  pwtrufal  14750