Theorem sselda 3227

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  pwntru  4289  elrel  4828  ffvresb  5810  1stdm  6344  tfrlem1  6473  tfrlemiubacc  6495  tfr1onlemubacc  6511  tfrcllemubacc  6524  erinxp  6777  fundmen  6980  supisolem  7206  ordiso2  7233  difinfsn  7298  ctssdc  7311  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  pw1m  7441  pw1on  7443  elprnql  7700  elprnqu  7701  suplocexprlemml  7935  axpre-suploclemres  8120  suprleubex  9133  un0addcl  9434  un0mulcl  9435  suprzclex  9577  supminfex  9830  infregelbex  9831  icoshftf1o  10225  elfzom1elfzo  10447  zpnn0elfzo  10451  seqfveqg  10739  seq3fveq  10740  monoord2  10747  seqsplitg  10750  seqcaopr2g  10755  seqf1oglem2a  10779  seqf1oglem2  10781  seqhomog  10791  seq3coll  11105  ccatass  11184  ccatrn  11185  ccatalpha  11189  pfxf  11262  swrdccatin2  11309  pfxccatin12lem2c  11310  rexanre  11780  rexico  11781  summodclem2a  11941  isumss  11951  fisumss  11952  fsum3cvg3  11956  fsumsplit  11967  fsum2dlemstep  11994  fisum0diag2  12007  fsumlessfi  12020  fsumabs  12025  telfsumo  12026  fsumparts  12030  fsumrelem  12031  fsumiun  12037  hashuni  12042  binom1dif  12047  isumsplit  12051  isumrpcl  12054  isumlessdc  12056  mertenslemi1  12095  clim2prod  12099  prodfrecap  12106  prodmodclem2a  12136  prodssdc  12149  fprodssdc  12150  fprodsplitdc  12156  fprod2dlemstep  12182  4sqlemffi  12968  4sqleminfi  12969  4sqlem11  12973  ennnfonelemfun  13037  ennnfonelemf1  13038  restid2  13330  gsumress  13477  gsumsplit1r  13480  issubmnd  13524  ress0g  13525  grpinvssd  13659  subginv  13767  issubg2m  13775  issubg4m  13779  subgintm  13784  ssnmz  13797  resghm  13846  conjnmz  13865  conjnmzb  13866  subcmnd  13919  ringidss  14041  invrpropdg  14162  subrg1  14244  subrginv  14250  subrgunit  14252  islss3  14392  lssintclm  14397  tgclb  14788  tgidm  14797  tgrest  14892  txcnp  14994  txdis1cn  15001  psmetres2  15056  blpnfctr  15162  xmetresbl  15163  mopni2  15206  mopni3  15207  rnblopn  15212  xmettx  15233  tgioo  15277  fsumcncntop  15290  climcncf  15307  suplociccreex  15347  suplociccex  15348  dedekindicc  15356  ivthdec  15367  dvfgg  15411  dvcnp2cntop  15422  dvaddxxbr  15424  dvcjbr  15431  dvmptfsum  15448  perfectlem2  15723  gausslemma2dlem2  15790  gausslemma2dlem3  15791  lgsquadlem2  15806  uhgredgm  15986  edgumgren  15992  edgusgren  16013  wlkres  16229  clwwlkccatlem  16250  pwtrufal  16598