Theorem sselda 3155

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 3154	. 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 3129

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 3135  df-ss 3142

This theorem is referenced by:  pwntru  4197  elrel  4726  ffvresb  5676  1stdm  6178  tfrlem1  6304  tfrlemiubacc  6326  tfr1onlemubacc  6342  tfrcllemubacc  6355  erinxp  6604  fundmen  6801  supisolem  7002  ordiso2  7029  difinfsn  7094  ctssdc  7107  exmidfodomrlemeldju  7193  exmidfodomrlemreseldju  7194  pw1on  7220  elprnql  7475  elprnqu  7476  suplocexprlemml  7710  axpre-suploclemres  7895  suprleubex  8905  un0addcl  9203  un0mulcl  9204  suprzclex  9345  supminfex  9591  infregelbex  9592  icoshftf1o  9985  elfzom1elfzo  10196  zpnn0elfzo  10200  seq3fveq  10464  monoord2  10470  seq3coll  10813  rexanre  11220  rexico  11221  summodclem2a  11380  isumss  11390  fisumss  11391  fsum3cvg3  11395  fsumsplit  11406  fsum2dlemstep  11433  fisum0diag2  11446  fsumlessfi  11459  fsumabs  11464  telfsumo  11465  fsumparts  11469  fsumrelem  11470  fsumiun  11476  hashuni  11481  binom1dif  11486  isumsplit  11490  isumrpcl  11493  isumlessdc  11495  mertenslemi1  11534  clim2prod  11538  prodfrecap  11545  prodmodclem2a  11575  prodssdc  11588  fprodssdc  11589  fprodsplitdc  11595  fprod2dlemstep  11621  ennnfonelemfun  12408  ennnfonelemf1  12409  restid2  12683  issubmnd  12773  grpinvssd  12875  subginv  12967  issubg2m  12975  issubg4m  12979  subgintm  12984  subcmnd  13029  ringidss  13112  invrpropdg  13217  tgclb  13347  tgidm  13356  tgrest  13451  txcnp  13553  txdis1cn  13560  psmetres2  13615  blpnfctr  13721  xmetresbl  13722  mopni2  13765  mopni3  13766  rnblopn  13771  xmettx  13792  tgioo  13828  fsumcncntop  13838  climcncf  13853  suplociccreex  13884  suplociccex  13885  dedekindicc  13893  ivthdec  13904  dvfgg  13939  dvcnp2cntop  13945  dvaddxxbr  13947  dvcjbr  13954  pwtrufal  14518