Theorem sselda 3242

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 3241	. 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 2205   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  pwntru  4317  elrel  4857  ffvresb  5845  1stdm  6389  tfrlem1  6552  tfrlemiubacc  6574  tfr1onlemubacc  6590  tfrcllemubacc  6603  erinxp  6856  fundmen  7060  supisolem  7312  ordiso2  7339  difinfsn  7404  ctssdc  7417  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  pw1m  7547  pw1on  7549  elprnql  7812  elprnqu  7813  suplocexprlemml  8047  axpre-suploclemres  8232  suprleubex  9245  un0addcl  9546  un0mulcl  9547  suprzclex  9694  supminfex  9947  infregelbex  9948  icoshftf1o  10343  elfzom1elfzo  10570  zpnn0elfzo  10574  seqfveqg  10864  seq3fveq  10865  monoord2  10872  seqsplitg  10875  seqcaopr2g  10880  seqf1oglem2a  10904  seqf1oglem2  10906  seqhomog  10916  seq3coll  11239  ccatass  11321  ccatrn  11322  ccatalpha  11326  pfxf  11399  swrdccatin2  11446  pfxccatin12lem2c  11447  rexanre  11930  rexico  11931  summodclem2a  12092  isumss  12102  fisumss  12103  fsum3cvg3  12107  fsumsplit  12118  fsum2dlemstep  12145  fisum0diag2  12158  fsumlessfi  12171  fsumabs  12176  telfsumo  12177  fsumparts  12181  fsumrelem  12182  fsumiun  12188  hashuni  12193  binom1dif  12198  isumsplit  12202  isumrpcl  12205  isumlessdc  12207  mertenslemi1  12246  clim2prod  12250  prodfrecap  12257  prodmodclem2a  12287  prodssdc  12300  fprodssdc  12301  fprodsplitdc  12307  fprod2dlemstep  12333  4sqlemffi  13119  4sqleminfi  13120  4sqlem11  13124  ballotfilemsel1i  13200  ballotfilemsima  13203  ballotfilemfrceq  13216  ennnfonelemfun  13252  ennnfonelemf1  13253  restid2  13545  gsumress  13658  gsumsplit1r  13661  issubmnd  13703  ress0g  13704  grpinvssd  13832  subginv  13934  issubg2m  13942  issubg4m  13946  subgintm  13951  ssnmz  13964  resghm  14013  conjnmz  14032  conjnmzb  14033  subcmnd  14086  ringidss  14272  invrpropdg  14394  subrg1  14477  subrginv  14483  subrgunit  14485  islss3  14653  lssintclm  14658  tgclb  15056  tgidm  15065  tgrest  15160  txcnp  15262  txdis1cn  15269  psmetres2  15324  blpnfctr  15430  xmetresbl  15431  mopni2  15474  mopni3  15475  rnblopn  15480  xmettx  15501  tgioo  15545  fsumcncntop  15558  climcncf  15575  suplociccreex  15615  suplociccex  15616  dedekindicc  15624  ivthdec  15635  dvfgg  15679  dvcnp2cntop  15690  dvaddxxbr  15692  dvcjbr  15699  dvmptfsum  15716  perfectlem2  15994  gausslemma2dlem2  16061  gausslemma2dlem3  16062  lgsquadlem2  16077  uhgredgm  16257  edgumgren  16263  edgusgren  16284  wlkres  16500  clwwlkccatlem  16521  pwtrufal  16897