Theorem sselda 3184

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  pwntru  4233  elrel  4766  ffvresb  5728  1stdm  6249  tfrlem1  6375  tfrlemiubacc  6397  tfr1onlemubacc  6413  tfrcllemubacc  6426  erinxp  6677  fundmen  6874  supisolem  7083  ordiso2  7110  difinfsn  7175  ctssdc  7188  exmidfodomrlemeldju  7280  exmidfodomrlemreseldju  7281  pw1on  7311  elprnql  7567  elprnqu  7568  suplocexprlemml  7802  axpre-suploclemres  7987  suprleubex  9000  un0addcl  9301  un0mulcl  9302  suprzclex  9443  supminfex  9690  infregelbex  9691  icoshftf1o  10085  elfzom1elfzo  10298  zpnn0elfzo  10302  seqfveqg  10589  seq3fveq  10590  monoord2  10597  seqsplitg  10600  seqcaopr2g  10605  seqf1oglem2a  10629  seqf1oglem2  10631  seqhomog  10641  seq3coll  10953  rexanre  11404  rexico  11405  summodclem2a  11565  isumss  11575  fisumss  11576  fsum3cvg3  11580  fsumsplit  11591  fsum2dlemstep  11618  fisum0diag2  11631  fsumlessfi  11644  fsumabs  11649  telfsumo  11650  fsumparts  11654  fsumrelem  11655  fsumiun  11661  hashuni  11666  binom1dif  11671  isumsplit  11675  isumrpcl  11678  isumlessdc  11680  mertenslemi1  11719  clim2prod  11723  prodfrecap  11730  prodmodclem2a  11760  prodssdc  11773  fprodssdc  11774  fprodsplitdc  11780  fprod2dlemstep  11806  4sqlemffi  12592  4sqleminfi  12593  4sqlem11  12597  ennnfonelemfun  12661  ennnfonelemf1  12662  restid2  12952  gsumress  13099  gsumsplit1r  13102  issubmnd  13146  ress0g  13147  grpinvssd  13281  subginv  13389  issubg2m  13397  issubg4m  13401  subgintm  13406  ssnmz  13419  resghm  13468  conjnmz  13487  conjnmzb  13488  subcmnd  13541  ringidss  13663  invrpropdg  13783  subrg1  13865  subrginv  13871  subrgunit  13873  islss3  14013  lssintclm  14018  tgclb  14409  tgidm  14418  tgrest  14513  txcnp  14615  txdis1cn  14622  psmetres2  14677  blpnfctr  14783  xmetresbl  14784  mopni2  14827  mopni3  14828  rnblopn  14833  xmettx  14854  tgioo  14898  fsumcncntop  14911  climcncf  14928  suplociccreex  14968  suplociccex  14969  dedekindicc  14977  ivthdec  14988  dvfgg  15032  dvcnp2cntop  15043  dvaddxxbr  15045  dvcjbr  15052  dvmptfsum  15069  perfectlem2  15344  gausslemma2dlem2  15411  gausslemma2dlem3  15412  lgsquadlem2  15427  pwtrufal  15752