Theorem sselda 3155

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2148   ⊆ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  pwntru  4199  elrel  4728  ffvresb  5679  1stdm  6182  tfrlem1  6308  tfrlemiubacc  6330  tfr1onlemubacc  6346  tfrcllemubacc  6359  erinxp  6608  fundmen  6805  supisolem  7006  ordiso2  7033  difinfsn  7098  ctssdc  7111  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  pw1on  7224  elprnql  7479  elprnqu  7480  suplocexprlemml  7714  axpre-suploclemres  7899  suprleubex  8910  un0addcl  9208  un0mulcl  9209  suprzclex  9350  supminfex  9596  infregelbex  9597  icoshftf1o  9990  elfzom1elfzo  10202  zpnn0elfzo  10206  seq3fveq  10470  monoord2  10476  seq3coll  10821  rexanre  11228  rexico  11229  summodclem2a  11388  isumss  11398  fisumss  11399  fsum3cvg3  11403  fsumsplit  11414  fsum2dlemstep  11441  fisum0diag2  11454  fsumlessfi  11467  fsumabs  11472  telfsumo  11473  fsumparts  11477  fsumrelem  11478  fsumiun  11484  hashuni  11489  binom1dif  11494  isumsplit  11498  isumrpcl  11501  isumlessdc  11503  mertenslemi1  11542  clim2prod  11546  prodfrecap  11553  prodmodclem2a  11583  prodssdc  11596  fprodssdc  11597  fprodsplitdc  11603  fprod2dlemstep  11629  ennnfonelemfun  12417  ennnfonelemf1  12418  restid2  12696  issubmnd  12842  ress0g  12843  grpinvssd  12946  subginv  13039  issubg2m  13047  issubg4m  13051  subgintm  13056  ssnmz  13069  subcmnd  13127  ringidss  13210  invrpropdg  13316  subrg1  13357  subrginv  13363  subrgunit  13365  tgclb  13501  tgidm  13510  tgrest  13605  txcnp  13707  txdis1cn  13714  psmetres2  13769  blpnfctr  13875  xmetresbl  13876  mopni2  13919  mopni3  13920  rnblopn  13925  xmettx  13946  tgioo  13982  fsumcncntop  13992  climcncf  14007  suplociccreex  14038  suplociccex  14039  dedekindicc  14047  ivthdec  14058  dvfgg  14093  dvcnp2cntop  14099  dvaddxxbr  14101  dvcjbr  14108  pwtrufal  14683