Theorem sselda 3026

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 1439   ⊆ wss 3000

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-11 1443  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-in 3006  df-ss 3013

This theorem is referenced by:  elrel  4553  ffvresb  5475  1stdm  5966  tfrlem1  6087  tfrlemiubacc  6109  tfr1onlemubacc  6125  tfrcllemubacc  6138  erinxp  6380  fundmen  6577  supisolem  6757  ordiso2  6782  exmidfodomrlemeldju  6879  exmidfodomrlemreseldju  6880  elprnql  7094  elprnqu  7095  suprleubex  8469  un0addcl  8760  un0mulcl  8761  suprzclex  8898  supminfex  9139  icoshftf1o  9462  elfzom1elfzo  9668  zpnn0elfzo  9672  iseqfveq  9948  seq3fveq  9949  monoord2  9959  iseqcoll  10301  rexanre  10707  rexico  10708  isummolem2a  10825  isumss  10837  fisumss  10838  fsum3cvg3  10843  fsumsplit  10855  fsum2dlemstep  10882  fisum0diag2  10895  fsumlessfi  10908  fsumabs  10913  telfsumo  10914  fsumparts  10918  fsumrelem  10919  fsumiun  10925  hashuni  10930  binom1dif  10935  isumsplit  10939  isumrpcl  10942  isumlessdc  10944  mertenslemi1  10983  restid2  11715  tgclb  11819  tgidm  11828  climcncf  11906