Theorem sselda 3180

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2164   ⊆ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  pwntru  4229  elrel  4762  ffvresb  5722  1stdm  6237  tfrlem1  6363  tfrlemiubacc  6385  tfr1onlemubacc  6401  tfrcllemubacc  6414  erinxp  6665  fundmen  6862  supisolem  7069  ordiso2  7096  difinfsn  7161  ctssdc  7174  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  pw1on  7288  elprnql  7543  elprnqu  7544  suplocexprlemml  7778  axpre-suploclemres  7963  suprleubex  8975  un0addcl  9276  un0mulcl  9277  suprzclex  9418  supminfex  9665  infregelbex  9666  icoshftf1o  10060  elfzom1elfzo  10273  zpnn0elfzo  10277  seqfveqg  10552  seq3fveq  10553  monoord2  10560  seqsplitg  10563  seqcaopr2g  10568  seqf1oglem2a  10592  seqf1oglem2  10594  seqhomog  10604  seq3coll  10916  rexanre  11367  rexico  11368  summodclem2a  11527  isumss  11537  fisumss  11538  fsum3cvg3  11542  fsumsplit  11553  fsum2dlemstep  11580  fisum0diag2  11593  fsumlessfi  11606  fsumabs  11611  telfsumo  11612  fsumparts  11616  fsumrelem  11617  fsumiun  11623  hashuni  11628  binom1dif  11633  isumsplit  11637  isumrpcl  11640  isumlessdc  11642  mertenslemi1  11681  clim2prod  11685  prodfrecap  11692  prodmodclem2a  11722  prodssdc  11735  fprodssdc  11736  fprodsplitdc  11742  fprod2dlemstep  11768  4sqlemffi  12537  4sqleminfi  12538  4sqlem11  12542  ennnfonelemfun  12577  ennnfonelemf1  12578  restid2  12862  gsumress  12981  gsumsplit1r  12984  issubmnd  13026  ress0g  13027  grpinvssd  13152  subginv  13254  issubg2m  13262  issubg4m  13266  subgintm  13271  ssnmz  13284  resghm  13333  conjnmz  13352  conjnmzb  13353  subcmnd  13406  ringidss  13528  invrpropdg  13648  subrg1  13730  subrginv  13736  subrgunit  13738  islss3  13878  lssintclm  13883  tgclb  14244  tgidm  14253  tgrest  14348  txcnp  14450  txdis1cn  14457  psmetres2  14512  blpnfctr  14618  xmetresbl  14619  mopni2  14662  mopni3  14663  rnblopn  14668  xmettx  14689  tgioo  14733  fsumcncntop  14746  climcncf  14763  suplociccreex  14803  suplociccex  14804  dedekindicc  14812  ivthdec  14823  dvfgg  14867  dvcnp2cntop  14878  dvaddxxbr  14880  dvcjbr  14887  dvmptfsum  14904  gausslemma2dlem2  15219  gausslemma2dlem3  15220  lgsquadlem2  15235  pwtrufal  15558