Theorem sselda 3224

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

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

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 3203  df-ss 3210

This theorem is referenced by:  pwntru  4282  elrel  4820  ffvresb  5797  1stdm  6326  tfrlem1  6452  tfrlemiubacc  6474  tfr1onlemubacc  6490  tfrcllemubacc  6503  erinxp  6754  fundmen  6957  supisolem  7171  ordiso2  7198  difinfsn  7263  ctssdc  7276  exmidfodomrlemeldju  7373  exmidfodomrlemreseldju  7374  pw1m  7405  pw1on  7407  elprnql  7664  elprnqu  7665  suplocexprlemml  7899  axpre-suploclemres  8084  suprleubex  9097  un0addcl  9398  un0mulcl  9399  suprzclex  9541  supminfex  9788  infregelbex  9789  icoshftf1o  10183  elfzom1elfzo  10404  zpnn0elfzo  10408  seqfveqg  10695  seq3fveq  10696  monoord2  10703  seqsplitg  10706  seqcaopr2g  10711  seqf1oglem2a  10735  seqf1oglem2  10737  seqhomog  10747  seq3coll  11059  ccatass  11138  ccatrn  11139  pfxf  11209  swrdccatin2  11256  pfxccatin12lem2c  11257  rexanre  11726  rexico  11727  summodclem2a  11887  isumss  11897  fisumss  11898  fsum3cvg3  11902  fsumsplit  11913  fsum2dlemstep  11940  fisum0diag2  11953  fsumlessfi  11966  fsumabs  11971  telfsumo  11972  fsumparts  11976  fsumrelem  11977  fsumiun  11983  hashuni  11988  binom1dif  11993  isumsplit  11997  isumrpcl  12000  isumlessdc  12002  mertenslemi1  12041  clim2prod  12045  prodfrecap  12052  prodmodclem2a  12082  prodssdc  12095  fprodssdc  12096  fprodsplitdc  12102  fprod2dlemstep  12128  4sqlemffi  12914  4sqleminfi  12915  4sqlem11  12919  ennnfonelemfun  12983  ennnfonelemf1  12984  restid2  13276  gsumress  13423  gsumsplit1r  13426  issubmnd  13470  ress0g  13471  grpinvssd  13605  subginv  13713  issubg2m  13721  issubg4m  13725  subgintm  13730  ssnmz  13743  resghm  13792  conjnmz  13811  conjnmzb  13812  subcmnd  13865  ringidss  13987  invrpropdg  14107  subrg1  14189  subrginv  14195  subrgunit  14197  islss3  14337  lssintclm  14342  tgclb  14733  tgidm  14742  tgrest  14837  txcnp  14939  txdis1cn  14946  psmetres2  15001  blpnfctr  15107  xmetresbl  15108  mopni2  15151  mopni3  15152  rnblopn  15157  xmettx  15178  tgioo  15222  fsumcncntop  15235  climcncf  15252  suplociccreex  15292  suplociccex  15293  dedekindicc  15301  ivthdec  15312  dvfgg  15356  dvcnp2cntop  15367  dvaddxxbr  15369  dvcjbr  15376  dvmptfsum  15393  perfectlem2  15668  gausslemma2dlem2  15735  gausslemma2dlem3  15736  lgsquadlem2  15751  uhgredgm  15928  edgumgren  15934  edgusgren  15955  pwtrufal  16322