Theorem sselda 3141

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2136   ⊆ wss 3115

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3121  df-ss 3128

This theorem is referenced by:  pwntru  4177  elrel  4705  ffvresb  5647  1stdm  6147  tfrlem1  6272  tfrlemiubacc  6294  tfr1onlemubacc  6310  tfrcllemubacc  6323  erinxp  6571  fundmen  6768  supisolem  6969  ordiso2  6996  difinfsn  7061  ctssdc  7074  exmidfodomrlemeldju  7151  exmidfodomrlemreseldju  7152  pw1on  7178  elprnql  7418  elprnqu  7419  suplocexprlemml  7653  axpre-suploclemres  7838  suprleubex  8845  un0addcl  9143  un0mulcl  9144  suprzclex  9285  supminfex  9531  infregelbex  9532  icoshftf1o  9923  elfzom1elfzo  10134  zpnn0elfzo  10138  seq3fveq  10402  monoord2  10408  seq3coll  10751  rexanre  11158  rexico  11159  summodclem2a  11318  isumss  11328  fisumss  11329  fsum3cvg3  11333  fsumsplit  11344  fsum2dlemstep  11371  fisum0diag2  11384  fsumlessfi  11397  fsumabs  11402  telfsumo  11403  fsumparts  11407  fsumrelem  11408  fsumiun  11414  hashuni  11419  binom1dif  11424  isumsplit  11428  isumrpcl  11431  isumlessdc  11433  mertenslemi1  11472  clim2prod  11476  prodfrecap  11483  prodmodclem2a  11513  prodssdc  11526  fprodssdc  11527  fprodsplitdc  11533  fprod2dlemstep  11559  ennnfonelemfun  12346  ennnfonelemf1  12347  restid2  12560  tgclb  12665  tgidm  12674  tgrest  12769  txcnp  12871  txdis1cn  12878  psmetres2  12933  blpnfctr  13039  xmetresbl  13040  mopni2  13083  mopni3  13084  rnblopn  13089  xmettx  13110  tgioo  13146  fsumcncntop  13156  climcncf  13171  suplociccreex  13202  suplociccex  13203  dedekindicc  13211  ivthdec  13222  dvfgg  13257  dvcnp2cntop  13263  dvaddxxbr  13265  dvcjbr  13272  pwtrufal  13837