Theorem sselda 3248

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  pwntru  4338  elrel  4879  ffvresb  5874  1stdm  6420  tfrlem1  6583  tfrlemiubacc  6605  tfr1onlemubacc  6621  tfrcllemubacc  6634  erinxp  6887  fundmen  7098  supisolem  7354  ordiso2  7381  difinfsn  7446  ctssdc  7459  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  pw1m  7589  pw1on  7591  elprnql  7854  elprnqu  7855  suplocexprlemml  8089  axpre-suploclemres  8274  suprleubex  9292  un0addcl  9607  un0mulcl  9608  suprzclex  9755  supminfex  10013  infregelbex  10014  icoshftf1o  10410  elfzom1elfzo  10638  zpnn0elfzo  10642  seqfveqg  10936  seq3fveq  10937  monoord2  10944  seqsplitg  10947  seqcaopr2g  10952  seqf1oglem2a  10976  seqf1oglem2  10978  seqhomog  10988  seq3coll  11316  ccatass  11398  ccatrn  11399  ccatalpha  11403  pfxf  11476  swrdccatin2  11523  pfxccatin12lem2c  11524  rexanre  12009  rexico  12010  summodclem2a  12173  isumss  12183  fisumss  12184  fsum3cvg3  12188  fsumsplit  12199  fsum2dlemstep  12226  fisum0diag2  12239  fsumlessfi  12252  fsumabs  12257  telfsumo  12258  fsumparts  12262  fsumrelem  12263  fsumiun  12269  hashuni  12274  binom1dif  12279  isumsplit  12283  isumrpcl  12286  isumlessdc  12288  mertenslemi1  12327  clim2prod  12331  prodfrecap  12338  prodmodclem2a  12368  prodssdc  12381  fprodssdc  12382  fprodsplitdc  12388  fprod2dlemstep  12414  4sqlemffi  13204  4sqleminfi  13205  4sqlem11  13209  ballotfilemsel1i  13314  ballotfilemsima  13317  ballotfilemfrceq  13330  ennnfonelemfun  13366  ennnfonelemf1  13367  restid2  13661  gzsumress  13771  gzsumsplit1r  13774  issubmnd  13814  ress0g  13815  grpinvssd  13941  subginv  14043  issubg2m  14051  issubg4m  14055  subgintm  14060  ssnmz  14073  resghm  14122  conjnmz  14141  conjnmzb  14142  cntzsgrpcl  14167  cntzsubm  14170  cntzmhm  14173  subcmnd  14227  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  gsum2dfilem2  14272  ringidss  14441  invrpropdg  14565  subrg1  14648  subrginv  14654  subrgunit  14656  islss3  14825  lssintclm  14830  issubassa2  15144  psrbaglefifi  15172  tgclb  15291  tgidm  15300  tgrest  15395  txcnp  15497  txdis1cn  15504  psmetres2  15559  blpnfctr  15665  xmetresbl  15666  mopni2  15709  mopni3  15710  rnblopn  15715  xmettx  15736  tgioo  15780  fsumcncntop  15793  climcncf  15810  suplociccreex  15850  suplociccex  15851  dedekindicc  15859  ivthdec  15870  dvfgg  15914  dvcnp2cntop  15925  dvaddxxbr  15927  dvcjbr  15934  dvmptfsum  15951  chtdif  16264  chtublem  16295  perfectlem2  16300  gausslemma2dlem2  16386  gausslemma2dlem3  16387  lgsquadlem2  16402  uhgredgm  16582  edgumgren  16588  edgusgren  16609  wlkres  16825  clwwlkccatlem  16846  pwtrufal  17232