Theorem sselda 3157

Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)

Hypothesis

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sselda	⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Proof of Theorem sselda

Step	Hyp	Ref	Expression
1		sseld.1	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2	1	sseld 3156	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148   ⊆ wss 3131

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 3137  df-ss 3144

This theorem is referenced by:  pwntru  4201  elrel  4730  ffvresb  5681  1stdm  6185  tfrlem1  6311  tfrlemiubacc  6333  tfr1onlemubacc  6349  tfrcllemubacc  6362  erinxp  6611  fundmen  6808  supisolem  7009  ordiso2  7036  difinfsn  7101  ctssdc  7114  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  pw1on  7227  elprnql  7482  elprnqu  7483  suplocexprlemml  7717  axpre-suploclemres  7902  suprleubex  8913  un0addcl  9211  un0mulcl  9212  suprzclex  9353  supminfex  9599  infregelbex  9600  icoshftf1o  9993  elfzom1elfzo  10205  zpnn0elfzo  10209  seq3fveq  10473  monoord2  10479  seq3coll  10824  rexanre  11231  rexico  11232  summodclem2a  11391  isumss  11401  fisumss  11402  fsum3cvg3  11406  fsumsplit  11417  fsum2dlemstep  11444  fisum0diag2  11457  fsumlessfi  11470  fsumabs  11475  telfsumo  11476  fsumparts  11480  fsumrelem  11481  fsumiun  11487  hashuni  11492  binom1dif  11497  isumsplit  11501  isumrpcl  11504  isumlessdc  11506  mertenslemi1  11545  clim2prod  11549  prodfrecap  11556  prodmodclem2a  11586  prodssdc  11599  fprodssdc  11600  fprodsplitdc  11606  fprod2dlemstep  11632  ennnfonelemfun  12420  ennnfonelemf1  12421  restid2  12702  issubmnd  12848  ress0g  12849  grpinvssd  12952  subginv  13046  issubg2m  13054  issubg4m  13058  subgintm  13063  ssnmz  13076  subcmnd  13134  ringidss  13217  invrpropdg  13323  subrg1  13357  subrginv  13363  subrgunit  13365  islss3  13471  lssintclm  13476  tgclb  13650  tgidm  13659  tgrest  13754  txcnp  13856  txdis1cn  13863  psmetres2  13918  blpnfctr  14024  xmetresbl  14025  mopni2  14068  mopni3  14069  rnblopn  14074  xmettx  14095  tgioo  14131  fsumcncntop  14141  climcncf  14156  suplociccreex  14187  suplociccex  14188  dedekindicc  14196  ivthdec  14207  dvfgg  14242  dvcnp2cntop  14248  dvaddxxbr  14250  dvcjbr  14257  pwtrufal  14832