Theorem sselda 3102

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1481   ⊆ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  pwntru  4130  elrel  4649  ffvresb  5591  1stdm  6088  tfrlem1  6213  tfrlemiubacc  6235  tfr1onlemubacc  6251  tfrcllemubacc  6264  erinxp  6511  fundmen  6708  supisolem  6903  ordiso2  6928  difinfsn  6993  ctssdc  7006  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  elprnql  7313  elprnqu  7314  suplocexprlemml  7548  axpre-suploclemres  7733  suprleubex  8736  un0addcl  9034  un0mulcl  9035  suprzclex  9173  supminfex  9419  icoshftf1o  9804  elfzom1elfzo  10011  zpnn0elfzo  10015  seq3fveq  10275  monoord2  10281  seq3coll  10617  rexanre  11024  rexico  11025  summodclem2a  11182  isumss  11192  fisumss  11193  fsum3cvg3  11197  fsumsplit  11208  fsum2dlemstep  11235  fisum0diag2  11248  fsumlessfi  11261  fsumabs  11266  telfsumo  11267  fsumparts  11271  fsumrelem  11272  fsumiun  11278  hashuni  11283  binom1dif  11288  isumsplit  11292  isumrpcl  11295  isumlessdc  11297  mertenslemi1  11336  clim2prod  11340  prodfrecap  11347  prodmodclem2a  11377  ennnfonelemfun  11966  ennnfonelemf1  11967  restid2  12168  tgclb  12273  tgidm  12282  tgrest  12377  txcnp  12479  txdis1cn  12486  psmetres2  12541  blpnfctr  12647  xmetresbl  12648  mopni2  12691  mopni3  12692  rnblopn  12697  xmettx  12718  tgioo  12754  fsumcncntop  12764  climcncf  12779  suplociccreex  12810  suplociccex  12811  dedekindicc  12819  ivthdec  12830  dvfgg  12865  dvcnp2cntop  12871  dvaddxxbr  12873  dvcjbr  12880  pwtrufal  13365