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  5798  1stdm  6328  tfrlem1  6454  tfrlemiubacc  6476  tfr1onlemubacc  6492  tfrcllemubacc  6505  erinxp  6756  fundmen  6959  supisolem  7175  ordiso2  7202  difinfsn  7267  ctssdc  7280  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  pw1m  7409  pw1on  7411  elprnql  7668  elprnqu  7669  suplocexprlemml  7903  axpre-suploclemres  8088  suprleubex  9101  un0addcl  9402  un0mulcl  9403  suprzclex  9545  supminfex  9792  infregelbex  9793  icoshftf1o  10187  elfzom1elfzo  10409  zpnn0elfzo  10413  seqfveqg  10700  seq3fveq  10701  monoord2  10708  seqsplitg  10711  seqcaopr2g  10716  seqf1oglem2a  10740  seqf1oglem2  10742  seqhomog  10752  seq3coll  11064  ccatass  11143  ccatrn  11144  pfxf  11214  swrdccatin2  11261  pfxccatin12lem2c  11262  rexanre  11731  rexico  11732  summodclem2a  11892  isumss  11902  fisumss  11903  fsum3cvg3  11907  fsumsplit  11918  fsum2dlemstep  11945  fisum0diag2  11958  fsumlessfi  11971  fsumabs  11976  telfsumo  11977  fsumparts  11981  fsumrelem  11982  fsumiun  11988  hashuni  11993  binom1dif  11998  isumsplit  12002  isumrpcl  12005  isumlessdc  12007  mertenslemi1  12046  clim2prod  12050  prodfrecap  12057  prodmodclem2a  12087  prodssdc  12100  fprodssdc  12101  fprodsplitdc  12107  fprod2dlemstep  12133  4sqlemffi  12919  4sqleminfi  12920  4sqlem11  12924  ennnfonelemfun  12988  ennnfonelemf1  12989  restid2  13281  gsumress  13428  gsumsplit1r  13431  issubmnd  13475  ress0g  13476  grpinvssd  13610  subginv  13718  issubg2m  13726  issubg4m  13730  subgintm  13735  ssnmz  13748  resghm  13797  conjnmz  13816  conjnmzb  13817  subcmnd  13870  ringidss  13992  invrpropdg  14113  subrg1  14195  subrginv  14201  subrgunit  14203  islss3  14343  lssintclm  14348  tgclb  14739  tgidm  14748  tgrest  14843  txcnp  14945  txdis1cn  14952  psmetres2  15007  blpnfctr  15113  xmetresbl  15114  mopni2  15157  mopni3  15158  rnblopn  15163  xmettx  15184  tgioo  15228  fsumcncntop  15241  climcncf  15258  suplociccreex  15298  suplociccex  15299  dedekindicc  15307  ivthdec  15318  dvfgg  15362  dvcnp2cntop  15373  dvaddxxbr  15375  dvcjbr  15382  dvmptfsum  15399  perfectlem2  15674  gausslemma2dlem2  15741  gausslemma2dlem3  15742  lgsquadlem2  15757  uhgredgm  15934  edgumgren  15940  edgusgren  15961  pwtrufal  16363