Theorem sselda 3228

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

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

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  pwntru  4295  elrel  4834  ffvresb  5818  1stdm  6354  tfrlem1  6517  tfrlemiubacc  6539  tfr1onlemubacc  6555  tfrcllemubacc  6568  erinxp  6821  fundmen  7024  supisolem  7250  ordiso2  7277  difinfsn  7342  ctssdc  7355  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  pw1m  7485  pw1on  7487  elprnql  7744  elprnqu  7745  suplocexprlemml  7979  axpre-suploclemres  8164  suprleubex  9176  un0addcl  9477  un0mulcl  9478  suprzclex  9622  supminfex  9875  infregelbex  9876  icoshftf1o  10270  elfzom1elfzo  10494  zpnn0elfzo  10498  seqfveqg  10786  seq3fveq  10787  monoord2  10794  seqsplitg  10797  seqcaopr2g  10802  seqf1oglem2a  10826  seqf1oglem2  10828  seqhomog  10838  seq3coll  11152  ccatass  11234  ccatrn  11235  ccatalpha  11239  pfxf  11312  swrdccatin2  11359  pfxccatin12lem2c  11360  rexanre  11843  rexico  11844  summodclem2a  12005  isumss  12015  fisumss  12016  fsum3cvg3  12020  fsumsplit  12031  fsum2dlemstep  12058  fisum0diag2  12071  fsumlessfi  12084  fsumabs  12089  telfsumo  12090  fsumparts  12094  fsumrelem  12095  fsumiun  12101  hashuni  12106  binom1dif  12111  isumsplit  12115  isumrpcl  12118  isumlessdc  12120  mertenslemi1  12159  clim2prod  12163  prodfrecap  12170  prodmodclem2a  12200  prodssdc  12213  fprodssdc  12214  fprodsplitdc  12220  fprod2dlemstep  12246  4sqlemffi  13032  4sqleminfi  13033  4sqlem11  13037  ennnfonelemfun  13101  ennnfonelemf1  13102  restid2  13394  gsumress  13541  gsumsplit1r  13544  issubmnd  13588  ress0g  13589  grpinvssd  13723  subginv  13831  issubg2m  13839  issubg4m  13843  subgintm  13848  ssnmz  13861  resghm  13910  conjnmz  13929  conjnmzb  13930  subcmnd  13983  ringidss  14106  invrpropdg  14227  subrg1  14309  subrginv  14315  subrgunit  14317  islss3  14458  lssintclm  14463  tgclb  14859  tgidm  14868  tgrest  14963  txcnp  15065  txdis1cn  15072  psmetres2  15127  blpnfctr  15233  xmetresbl  15234  mopni2  15277  mopni3  15278  rnblopn  15283  xmettx  15304  tgioo  15348  fsumcncntop  15361  climcncf  15378  suplociccreex  15418  suplociccex  15419  dedekindicc  15427  ivthdec  15438  dvfgg  15482  dvcnp2cntop  15493  dvaddxxbr  15495  dvcjbr  15502  dvmptfsum  15519  perfectlem2  15797  gausslemma2dlem2  15864  gausslemma2dlem3  15865  lgsquadlem2  15880  uhgredgm  16060  edgumgren  16066  edgusgren  16087  wlkres  16303  clwwlkccatlem  16324  pwtrufal  16702