Theorem sselda 3147

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

Syntax hints:   → wi 4   ∧ wa 103   ∈ wcel 2141   ⊆ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  pwntru  4185  elrel  4713  ffvresb  5659  1stdm  6161  tfrlem1  6287  tfrlemiubacc  6309  tfr1onlemubacc  6325  tfrcllemubacc  6338  erinxp  6587  fundmen  6784  supisolem  6985  ordiso2  7012  difinfsn  7077  ctssdc  7090  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  pw1on  7203  elprnql  7443  elprnqu  7444  suplocexprlemml  7678  axpre-suploclemres  7863  suprleubex  8870  un0addcl  9168  un0mulcl  9169  suprzclex  9310  supminfex  9556  infregelbex  9557  icoshftf1o  9948  elfzom1elfzo  10159  zpnn0elfzo  10163  seq3fveq  10427  monoord2  10433  seq3coll  10777  rexanre  11184  rexico  11185  summodclem2a  11344  isumss  11354  fisumss  11355  fsum3cvg3  11359  fsumsplit  11370  fsum2dlemstep  11397  fisum0diag2  11410  fsumlessfi  11423  fsumabs  11428  telfsumo  11429  fsumparts  11433  fsumrelem  11434  fsumiun  11440  hashuni  11445  binom1dif  11450  isumsplit  11454  isumrpcl  11457  isumlessdc  11459  mertenslemi1  11498  clim2prod  11502  prodfrecap  11509  prodmodclem2a  11539  prodssdc  11552  fprodssdc  11553  fprodsplitdc  11559  fprod2dlemstep  11585  ennnfonelemfun  12372  ennnfonelemf1  12373  restid2  12588  tgclb  12859  tgidm  12868  tgrest  12963  txcnp  13065  txdis1cn  13072  psmetres2  13127  blpnfctr  13233  xmetresbl  13234  mopni2  13277  mopni3  13278  rnblopn  13283  xmettx  13304  tgioo  13340  fsumcncntop  13350  climcncf  13365  suplociccreex  13396  suplociccex  13397  dedekindicc  13405  ivthdec  13416  dvfgg  13451  dvcnp2cntop  13457  dvaddxxbr  13459  dvcjbr  13466  pwtrufal  14030