Theorem sselda 3224

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 3223	. 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 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  pwntru  4283  elrel  4821  ffvresb  5800  1stdm  6334  tfrlem1  6460  tfrlemiubacc  6482  tfr1onlemubacc  6498  tfrcllemubacc  6511  erinxp  6764  fundmen  6967  supisolem  7186  ordiso2  7213  difinfsn  7278  ctssdc  7291  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  pw1m  7420  pw1on  7422  elprnql  7679  elprnqu  7680  suplocexprlemml  7914  axpre-suploclemres  8099  suprleubex  9112  un0addcl  9413  un0mulcl  9414  suprzclex  9556  supminfex  9804  infregelbex  9805  icoshftf1o  10199  elfzom1elfzo  10421  zpnn0elfzo  10425  seqfveqg  10712  seq3fveq  10713  monoord2  10720  seqsplitg  10723  seqcaopr2g  10728  seqf1oglem2a  10752  seqf1oglem2  10754  seqhomog  10764  seq3coll  11077  ccatass  11156  ccatrn  11157  ccatalpha  11161  pfxf  11230  swrdccatin2  11277  pfxccatin12lem2c  11278  rexanre  11747  rexico  11748  summodclem2a  11908  isumss  11918  fisumss  11919  fsum3cvg3  11923  fsumsplit  11934  fsum2dlemstep  11961  fisum0diag2  11974  fsumlessfi  11987  fsumabs  11992  telfsumo  11993  fsumparts  11997  fsumrelem  11998  fsumiun  12004  hashuni  12009  binom1dif  12014  isumsplit  12018  isumrpcl  12021  isumlessdc  12023  mertenslemi1  12062  clim2prod  12066  prodfrecap  12073  prodmodclem2a  12103  prodssdc  12116  fprodssdc  12117  fprodsplitdc  12123  fprod2dlemstep  12149  4sqlemffi  12935  4sqleminfi  12936  4sqlem11  12940  ennnfonelemfun  13004  ennnfonelemf1  13005  restid2  13297  gsumress  13444  gsumsplit1r  13447  issubmnd  13491  ress0g  13492  grpinvssd  13626  subginv  13734  issubg2m  13742  issubg4m  13746  subgintm  13751  ssnmz  13764  resghm  13813  conjnmz  13832  conjnmzb  13833  subcmnd  13886  ringidss  14008  invrpropdg  14129  subrg1  14211  subrginv  14217  subrgunit  14219  islss3  14359  lssintclm  14364  tgclb  14755  tgidm  14764  tgrest  14859  txcnp  14961  txdis1cn  14968  psmetres2  15023  blpnfctr  15129  xmetresbl  15130  mopni2  15173  mopni3  15174  rnblopn  15179  xmettx  15200  tgioo  15244  fsumcncntop  15257  climcncf  15274  suplociccreex  15314  suplociccex  15315  dedekindicc  15323  ivthdec  15334  dvfgg  15378  dvcnp2cntop  15389  dvaddxxbr  15391  dvcjbr  15398  dvmptfsum  15415  perfectlem2  15690  gausslemma2dlem2  15757  gausslemma2dlem3  15758  lgsquadlem2  15773  uhgredgm  15950  edgumgren  15956  edgusgren  15977  wlkres  16123  clwwlkccatlem  16143  pwtrufal  16450