Theorem sselda 3183

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 3182	. 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  4232  elrel  4765  ffvresb  5725  1stdm  6240  tfrlem1  6366  tfrlemiubacc  6388  tfr1onlemubacc  6404  tfrcllemubacc  6417  erinxp  6668  fundmen  6865  supisolem  7074  ordiso2  7101  difinfsn  7166  ctssdc  7179  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  pw1on  7293  elprnql  7548  elprnqu  7549  suplocexprlemml  7783  axpre-suploclemres  7968  suprleubex  8981  un0addcl  9282  un0mulcl  9283  suprzclex  9424  supminfex  9671  infregelbex  9672  icoshftf1o  10066  elfzom1elfzo  10279  zpnn0elfzo  10283  seqfveqg  10570  seq3fveq  10571  monoord2  10578  seqsplitg  10581  seqcaopr2g  10586  seqf1oglem2a  10610  seqf1oglem2  10612  seqhomog  10622  seq3coll  10934  rexanre  11385  rexico  11386  summodclem2a  11546  isumss  11556  fisumss  11557  fsum3cvg3  11561  fsumsplit  11572  fsum2dlemstep  11599  fisum0diag2  11612  fsumlessfi  11625  fsumabs  11630  telfsumo  11631  fsumparts  11635  fsumrelem  11636  fsumiun  11642  hashuni  11647  binom1dif  11652  isumsplit  11656  isumrpcl  11659  isumlessdc  11661  mertenslemi1  11700  clim2prod  11704  prodfrecap  11711  prodmodclem2a  11741  prodssdc  11754  fprodssdc  11755  fprodsplitdc  11761  fprod2dlemstep  11787  4sqlemffi  12565  4sqleminfi  12566  4sqlem11  12570  ennnfonelemfun  12634  ennnfonelemf1  12635  restid2  12919  gsumress  13038  gsumsplit1r  13041  issubmnd  13083  ress0g  13084  grpinvssd  13209  subginv  13311  issubg2m  13319  issubg4m  13323  subgintm  13328  ssnmz  13341  resghm  13390  conjnmz  13409  conjnmzb  13410  subcmnd  13463  ringidss  13585  invrpropdg  13705  subrg1  13787  subrginv  13793  subrgunit  13795  islss3  13935  lssintclm  13940  tgclb  14301  tgidm  14310  tgrest  14405  txcnp  14507  txdis1cn  14514  psmetres2  14569  blpnfctr  14675  xmetresbl  14676  mopni2  14719  mopni3  14720  rnblopn  14725  xmettx  14746  tgioo  14790  fsumcncntop  14803  climcncf  14820  suplociccreex  14860  suplociccex  14861  dedekindicc  14869  ivthdec  14880  dvfgg  14924  dvcnp2cntop  14935  dvaddxxbr  14937  dvcjbr  14944  dvmptfsum  14961  perfectlem2  15236  gausslemma2dlem2  15303  gausslemma2dlem3  15304  lgsquadlem2  15319  pwtrufal  15642