Theorem sselda 3197

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177   ⊆ wss 3170

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3176  df-ss 3183

This theorem is referenced by:  pwntru  4250  elrel  4784  ffvresb  5755  1stdm  6280  tfrlem1  6406  tfrlemiubacc  6428  tfr1onlemubacc  6444  tfrcllemubacc  6457  erinxp  6708  fundmen  6911  supisolem  7124  ordiso2  7151  difinfsn  7216  ctssdc  7229  exmidfodomrlemeldju  7322  exmidfodomrlemreseldju  7323  pw1on  7353  elprnql  7609  elprnqu  7610  suplocexprlemml  7844  axpre-suploclemres  8029  suprleubex  9042  un0addcl  9343  un0mulcl  9344  suprzclex  9486  supminfex  9733  infregelbex  9734  icoshftf1o  10128  elfzom1elfzo  10349  zpnn0elfzo  10353  seqfveqg  10640  seq3fveq  10641  monoord2  10648  seqsplitg  10651  seqcaopr2g  10656  seqf1oglem2a  10680  seqf1oglem2  10682  seqhomog  10692  seq3coll  11004  ccatass  11082  ccatrn  11083  pfxf  11153  rexanre  11601  rexico  11602  summodclem2a  11762  isumss  11772  fisumss  11773  fsum3cvg3  11777  fsumsplit  11788  fsum2dlemstep  11815  fisum0diag2  11828  fsumlessfi  11841  fsumabs  11846  telfsumo  11847  fsumparts  11851  fsumrelem  11852  fsumiun  11858  hashuni  11863  binom1dif  11868  isumsplit  11872  isumrpcl  11875  isumlessdc  11877  mertenslemi1  11916  clim2prod  11920  prodfrecap  11927  prodmodclem2a  11957  prodssdc  11970  fprodssdc  11971  fprodsplitdc  11977  fprod2dlemstep  12003  4sqlemffi  12789  4sqleminfi  12790  4sqlem11  12794  ennnfonelemfun  12858  ennnfonelemf1  12859  restid2  13150  gsumress  13297  gsumsplit1r  13300  issubmnd  13344  ress0g  13345  grpinvssd  13479  subginv  13587  issubg2m  13595  issubg4m  13599  subgintm  13604  ssnmz  13617  resghm  13666  conjnmz  13685  conjnmzb  13686  subcmnd  13739  ringidss  13861  invrpropdg  13981  subrg1  14063  subrginv  14069  subrgunit  14071  islss3  14211  lssintclm  14216  tgclb  14607  tgidm  14616  tgrest  14711  txcnp  14813  txdis1cn  14820  psmetres2  14875  blpnfctr  14981  xmetresbl  14982  mopni2  15025  mopni3  15026  rnblopn  15031  xmettx  15052  tgioo  15096  fsumcncntop  15109  climcncf  15126  suplociccreex  15166  suplociccex  15167  dedekindicc  15175  ivthdec  15186  dvfgg  15230  dvcnp2cntop  15241  dvaddxxbr  15243  dvcjbr  15250  dvmptfsum  15267  perfectlem2  15542  gausslemma2dlem2  15609  gausslemma2dlem3  15610  lgsquadlem2  15625  pwtrufal  16069