Theorem sselda 3224

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  pwntru  4283  elrel  4821  ffvresb  5800  1stdm  6334  tfrlem1  6460  tfrlemiubacc  6482  tfr1onlemubacc  6498  tfrcllemubacc  6511  erinxp  6764  fundmen  6967  supisolem  7186  ordiso2  7213  difinfsn  7278  ctssdc  7291  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  pw1m  7420  pw1on  7422  elprnql  7679  elprnqu  7680  suplocexprlemml  7914  axpre-suploclemres  8099  suprleubex  9112  un0addcl  9413  un0mulcl  9414  suprzclex  9556  supminfex  9804  infregelbex  9805  icoshftf1o  10199  elfzom1elfzo  10421  zpnn0elfzo  10425  seqfveqg  10712  seq3fveq  10713  monoord2  10720  seqsplitg  10723  seqcaopr2g  10728  seqf1oglem2a  10752  seqf1oglem2  10754  seqhomog  10764  seq3coll  11077  ccatass  11156  ccatrn  11157  ccatalpha  11161  pfxf  11229  swrdccatin2  11276  pfxccatin12lem2c  11277  rexanre  11746  rexico  11747  summodclem2a  11907  isumss  11917  fisumss  11918  fsum3cvg3  11922  fsumsplit  11933  fsum2dlemstep  11960  fisum0diag2  11973  fsumlessfi  11986  fsumabs  11991  telfsumo  11992  fsumparts  11996  fsumrelem  11997  fsumiun  12003  hashuni  12008  binom1dif  12013  isumsplit  12017  isumrpcl  12020  isumlessdc  12022  mertenslemi1  12061  clim2prod  12065  prodfrecap  12072  prodmodclem2a  12102  prodssdc  12115  fprodssdc  12116  fprodsplitdc  12122  fprod2dlemstep  12148  4sqlemffi  12934  4sqleminfi  12935  4sqlem11  12939  ennnfonelemfun  13003  ennnfonelemf1  13004  restid2  13296  gsumress  13443  gsumsplit1r  13446  issubmnd  13490  ress0g  13491  grpinvssd  13625  subginv  13733  issubg2m  13741  issubg4m  13745  subgintm  13750  ssnmz  13763  resghm  13812  conjnmz  13831  conjnmzb  13832  subcmnd  13885  ringidss  14007  invrpropdg  14128  subrg1  14210  subrginv  14216  subrgunit  14218  islss3  14358  lssintclm  14363  tgclb  14754  tgidm  14763  tgrest  14858  txcnp  14960  txdis1cn  14967  psmetres2  15022  blpnfctr  15128  xmetresbl  15129  mopni2  15172  mopni3  15173  rnblopn  15178  xmettx  15199  tgioo  15243  fsumcncntop  15256  climcncf  15273  suplociccreex  15313  suplociccex  15314  dedekindicc  15322  ivthdec  15333  dvfgg  15377  dvcnp2cntop  15388  dvaddxxbr  15390  dvcjbr  15397  dvmptfsum  15414  perfectlem2  15689  gausslemma2dlem2  15756  gausslemma2dlem3  15757  lgsquadlem2  15772  uhgredgm  15949  edgumgren  15955  edgusgren  15976  wlkres  16118  clwwlkccatlem  16137  pwtrufal  16422