Theorem sselda 3225

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

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

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 3204  df-ss 3211

This theorem is referenced by:  pwntru  4287  elrel  4826  ffvresb  5806  1stdm  6340  tfrlem1  6469  tfrlemiubacc  6491  tfr1onlemubacc  6507  tfrcllemubacc  6520  erinxp  6773  fundmen  6976  supisolem  7198  ordiso2  7225  difinfsn  7290  ctssdc  7303  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  pw1m  7432  pw1on  7434  elprnql  7691  elprnqu  7692  suplocexprlemml  7926  axpre-suploclemres  8111  suprleubex  9124  un0addcl  9425  un0mulcl  9426  suprzclex  9568  supminfex  9821  infregelbex  9822  icoshftf1o  10216  elfzom1elfzo  10438  zpnn0elfzo  10442  seqfveqg  10730  seq3fveq  10731  monoord2  10738  seqsplitg  10741  seqcaopr2g  10746  seqf1oglem2a  10770  seqf1oglem2  10772  seqhomog  10782  seq3coll  11096  ccatass  11175  ccatrn  11176  ccatalpha  11180  pfxf  11253  swrdccatin2  11300  pfxccatin12lem2c  11301  rexanre  11771  rexico  11772  summodclem2a  11932  isumss  11942  fisumss  11943  fsum3cvg3  11947  fsumsplit  11958  fsum2dlemstep  11985  fisum0diag2  11998  fsumlessfi  12011  fsumabs  12016  telfsumo  12017  fsumparts  12021  fsumrelem  12022  fsumiun  12028  hashuni  12033  binom1dif  12038  isumsplit  12042  isumrpcl  12045  isumlessdc  12047  mertenslemi1  12086  clim2prod  12090  prodfrecap  12097  prodmodclem2a  12127  prodssdc  12140  fprodssdc  12141  fprodsplitdc  12147  fprod2dlemstep  12173  4sqlemffi  12959  4sqleminfi  12960  4sqlem11  12964  ennnfonelemfun  13028  ennnfonelemf1  13029  restid2  13321  gsumress  13468  gsumsplit1r  13471  issubmnd  13515  ress0g  13516  grpinvssd  13650  subginv  13758  issubg2m  13766  issubg4m  13770  subgintm  13775  ssnmz  13788  resghm  13837  conjnmz  13856  conjnmzb  13857  subcmnd  13910  ringidss  14032  invrpropdg  14153  subrg1  14235  subrginv  14241  subrgunit  14243  islss3  14383  lssintclm  14388  tgclb  14779  tgidm  14788  tgrest  14883  txcnp  14985  txdis1cn  14992  psmetres2  15047  blpnfctr  15153  xmetresbl  15154  mopni2  15197  mopni3  15198  rnblopn  15203  xmettx  15224  tgioo  15268  fsumcncntop  15281  climcncf  15298  suplociccreex  15338  suplociccex  15339  dedekindicc  15347  ivthdec  15358  dvfgg  15402  dvcnp2cntop  15413  dvaddxxbr  15415  dvcjbr  15422  dvmptfsum  15439  perfectlem2  15714  gausslemma2dlem2  15781  gausslemma2dlem3  15782  lgsquadlem2  15797  uhgredgm  15975  edgumgren  15981  edgusgren  16002  wlkres  16174  clwwlkccatlem  16195  pwtrufal  16534