Theorem sselda 3227

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 3226	. 2 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	2	imp 124	1 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → 𝐶 ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  pwntru  4289  elrel  4828  ffvresb  5810  1stdm  6345  tfrlem1  6474  tfrlemiubacc  6496  tfr1onlemubacc  6512  tfrcllemubacc  6525  erinxp  6778  fundmen  6981  supisolem  7207  ordiso2  7234  difinfsn  7299  ctssdc  7312  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  pw1m  7442  pw1on  7444  elprnql  7701  elprnqu  7702  suplocexprlemml  7936  axpre-suploclemres  8121  suprleubex  9134  un0addcl  9435  un0mulcl  9436  suprzclex  9578  supminfex  9831  infregelbex  9832  icoshftf1o  10226  elfzom1elfzo  10449  zpnn0elfzo  10453  seqfveqg  10741  seq3fveq  10742  monoord2  10749  seqsplitg  10752  seqcaopr2g  10757  seqf1oglem2a  10781  seqf1oglem2  10783  seqhomog  10793  seq3coll  11107  ccatass  11189  ccatrn  11190  ccatalpha  11194  pfxf  11267  swrdccatin2  11314  pfxccatin12lem2c  11315  rexanre  11798  rexico  11799  summodclem2a  11960  isumss  11970  fisumss  11971  fsum3cvg3  11975  fsumsplit  11986  fsum2dlemstep  12013  fisum0diag2  12026  fsumlessfi  12039  fsumabs  12044  telfsumo  12045  fsumparts  12049  fsumrelem  12050  fsumiun  12056  hashuni  12061  binom1dif  12066  isumsplit  12070  isumrpcl  12073  isumlessdc  12075  mertenslemi1  12114  clim2prod  12118  prodfrecap  12125  prodmodclem2a  12155  prodssdc  12168  fprodssdc  12169  fprodsplitdc  12175  fprod2dlemstep  12201  4sqlemffi  12987  4sqleminfi  12988  4sqlem11  12992  ennnfonelemfun  13056  ennnfonelemf1  13057  restid2  13349  gsumress  13496  gsumsplit1r  13499  issubmnd  13543  ress0g  13544  grpinvssd  13678  subginv  13786  issubg2m  13794  issubg4m  13798  subgintm  13803  ssnmz  13816  resghm  13865  conjnmz  13884  conjnmzb  13885  subcmnd  13938  ringidss  14061  invrpropdg  14182  subrg1  14264  subrginv  14270  subrgunit  14272  islss3  14412  lssintclm  14417  tgclb  14808  tgidm  14817  tgrest  14912  txcnp  15014  txdis1cn  15021  psmetres2  15076  blpnfctr  15182  xmetresbl  15183  mopni2  15226  mopni3  15227  rnblopn  15232  xmettx  15253  tgioo  15297  fsumcncntop  15310  climcncf  15327  suplociccreex  15367  suplociccex  15368  dedekindicc  15376  ivthdec  15387  dvfgg  15431  dvcnp2cntop  15442  dvaddxxbr  15444  dvcjbr  15451  dvmptfsum  15468  perfectlem2  15743  gausslemma2dlem2  15810  gausslemma2dlem3  15811  lgsquadlem2  15826  uhgredgm  16006  edgumgren  16012  edgusgren  16033  wlkres  16249  clwwlkccatlem  16270  pwtrufal  16649