Theorem sseld 3982

Description: Membership deduction from subclass relationship. (Contributed by NM, 15-Nov-1995.)

Hypothesis

Ref	Expression
sseld.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sseld	⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem sseld

Step	Hyp	Ref	Expression
1		sseld.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssel 3976	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sselda  3983  sseldd  3984  ssneld  3985  elelpwi  4613  ssbrd  5192  uniopel  5517  exopxfr2  5845  dmrnssfld  5970  preddowncl  6334  opelf  6753  elfvunirn  6924  fvimacnv  7055  ffvelcdm  7084  fnsnr  7163  f1imass  7263  onminex  7790  xpord2pred  8131  extmptsuppeq  8173  suppssr  8181  suppssrg  8182  dftpos3  8229  wfrlem16OLD  8324  oa00  8559  omordi  8566  omlimcl  8578  omeulem1  8582  nnmordi  8631  mapsnd  8880  ixpf  8914  pw2f1olem  9076  pssnn  9168  pssnnOLD  9265  findcard3  9285  findcard3OLD  9286  ixpfi2  9350  fissuni  9357  elfiun  9425  dffi3  9426  ordiso2  9510  ordtypelem7  9519  ixpiunwdom  9585  inf3lem2  9624  cantnfp1lem3  9675  cantnfp1  9676  cantnflem1  9684  cantnf  9688  trcl  9723  r1ordg  9773  rankelb  9819  rankuni2b  9848  rankval4  9862  tcrank  9879  cplem1  9884  carduniima  10091  alephfp  10103  kmlem2  10146  isf32lem3  10350  domtriomlem  10437  axdc3lem2  10446  zorn2lem7  10497  ttukeylem6  10509  iundom2g  10535  fpwwe2lem12  10637  tskss  10753  tskr1om2  10763  inatsk  10773  gruss  10791  gruel  10798  grur1  10815  prlem934  11028  ltexprlem7  11037  supsr  11107  dedekind  11377  supadd  12182  supmullem2  12185  uzind  12654  iccsplit  13462  elfz0add  13600  predfz  13626  fsuppmapnn0fiub  13956  ccatval2  14528  swrdswrd  14655  pfxccatin12lem2a  14677  swrdccatin2  14679  pfxccatpfx2  14687  cshimadifsn0  14781  01sqrexlem6  15194  isercolllem2  15612  fsumcvg  15658  isumrpcl  15789  fprodcvg  15874  rpnnen2lem4  16160  fproddvdsd  16278  saddisj  16406  sadass  16412  bitsshft  16416  smuval2  16423  smupvallem  16424  smu01lem  16426  smueqlem  16431  reumodprminv  16737  ramub1lem1  16959  firest  17378  mrissmrid  17585  initoeu2lem0  17963  acsfiindd  18506  acsmapd  18507  dirge  18556  issubmnd  18652  issubg2  19021  eqgid  19060  cyccom  19080  dprdff  19882  dprddisj2  19909  ablfac1c  19941  subrgdvds  20333  issubrg2  20339  lssssr  20564  lssats2  20611  lbspss  20693  lsmelval2  20696  lspprat  20766  lbsextlem2  20772  lbsextlem3  20773  lpigen  20894  psgndiflemB  21153  lsmcss  21245  obselocv  21283  f1lindf  21377  issubassa3  21420  mplcoe5lem  21594  mdetdiaglem  22100  cpmadugsumlemF  22378  toprntopon  22427  elcls  22577  clsndisj  22579  elcls3  22587  neindisj  22621  lpval  22643  lpsscls  22645  lpss3  22648  maxlp  22651  restntr  22686  ordtbas2  22695  ordtbas  22696  pnfnei  22724  mnfnei  22725  cncls2  22777  lmcnp  22808  lpcls  22868  hauscmplem  22910  2ndcdisj  22960  kgen2ss  23059  txuni2  23069  ptpjpre1  23075  tx1cn  23113  tx2cn  23114  prdstopn  23132  txlm  23152  imasnopn  23194  imasncld  23195  imasncls  23196  tgqtop  23216  regr1lem  23243  fgss2  23378  uzfbas  23402  ufilmax  23411  uffix2  23428  ufildr  23435  fmfnfmlem1  23458  fmco  23465  flimrest  23487  fclsopn  23518  fclscf  23529  flimfcls  23530  alexsubALTlem4  23554  qustgplem  23625  imasf1oxms  23998  prdsbl  24000  metrest  24033  iccntr  24337  reconnlem2  24343  caucfil  24800  caussi  24814  bcthlem5  24845  ovoliunlem1  25019  shft2rab  25025  sca2rab  25029  ovolicc2  25039  vitalilem2  25126  vitalilem5  25129  mbfinf  25182  i1f1lem  25206  mbfi1fseqlem4  25236  itgss  25329  itgcn  25362  c1liplem1  25513  c1lip1  25514  c1lip3  25516  ply1remlem  25680  plyexmo  25826  lgamucov  26542  fsumvma  26716  logfaclbnd  26725  sltres  27165  nosepssdm  27189  nodenselem8  27194  nosupno  27206  nosupbday  27208  noinfbday  27223  elmade  27362  oldssmade  27372  mulsproplem13  27584  mulsproplem14  27585  precsexlem10  27662  axlowdimlem16  28215  axcontlem9  28230  edgupgr  28394  upgredg  28397  subgreldmiedg  28540  upgrres1  28570  crctcshwlkn0lem2  29065  wwlksnred  29146  clwwlkccatlem  29242  clwwlkf  29300  wwlksubclwwlk  29311  eupth2lems  29491  sspmval  29986  sspimsval  29991  ubthlem1  30123  shsubcl  30473  shorth  30548  elspansn3  30825  elnlfn  31181  elpjrn  31443  sumdmdlem2  31672  eqrrabd  31741  nfpconfp  31856  fimarab  31868  supssd  31934  infssd  31935  xrofsup  31980  elrspunidl  32546  ressply1mon1p  32657  cmpcref  32830  zarclsiin  32851  cntmeas  33224  1stmbfm  33259  2ndmbfm  33260  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemodife  33496  ballotlemimin  33504  bnj1171  34011  bnj1280  34031  subgrwlk  34123  gonarlem  34385  goalrlem  34387  mrsubrn  34504  elfzm12  34660  ontgval  35316  bj-restuni  35978  pibt2  36298  lindsenlbs  36483  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  itg2addnclem  36539  itg2addnclem2  36540  ftc1anclem7  36567  ismtyima  36671  lshpkr  37987  psubatN  38626  elpaddn0  38671  pclfinN  38771  diael  39914  dia2dimlem12  39946  dicelval1stN  40059  dicelval2nd  40060  dib2dim  40114  dih2dimbALTN  40116  dihlspsnssN  40203  dvh1dim  40313  lcfrvalsnN  40412  mapdrvallem2  40516  mapdpglem2  40544  hdmap10lem  40710  hdmap11lem2  40713  hdmapoc  40802  sticksstones3  40964  sticksstones17  40979  sticksstones18  40980  isnacs3  41448  aomclem2  41797  kelac1  41805  rngunsnply  41915  safesnsupfiub  42167  intabssd  42270  iunrelexp0  42453  rfovcnvf1od  42755  rfovcnvfvd  42758  fsovrfovd  42760  clsk1indlem3  42794  neik0pk1imk0  42798  ntrneineine0lem  42834  ntrneiel2  42837  ntrneikb  42845  ntrneik4w  42851  mnuop3d  43030  dvconstbi  43093  expgrowth  43094  climsuselem1  44323  climsuse  44324  limcresiooub  44358  iblsplit  44682  iblspltprt  44689  stoweidlem62  44778  stirlinglem11  44800  fourierdlem41  44864  qndenserrnbllem  45010  sge0fodjrnlem  45132  sssmf  45454  smflimsuplem7  45542  fafvelcdm  45878  fafv2elcdm  45942  smonoord  46039  iccpartiltu  46090  iccpartigtl  46091  iccpartiun  46102  iccpartdisj  46105  bgoldbtbndlem2  46474  c0rnghm  46712  issubrng2  46737  rnglidlmmgm  46756  rnglidlmsgrp  46757  rnglidlrng  46758  lidldomn1  46823  rnghmsscmap  46872  rngcsect  46878  funcrngcsetc  46896  rhmsscmap  46918  rhmsscrnghm  46924  ringcsect  46929  funcringcsetc  46933  funcringcsetcALTV2lem9  46942  rhmsubclem4  46987  rhmsubcALTVlem4  47005  lincresunit3lem1  47160  setrec1  47736  setis  47743  vsetrec  47748  pgindnf  47761