Theorem sseld 4007

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 4002	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-clel 2819  df-ss 3993

This theorem is referenced by:  sselda  4008  sseldd  4009  ssneld  4010  eqrrabd  4109  elelpwi  4632  ssbrd  5209  uniopel  5535  exopxfr2  5869  dmrnssfld  5996  preddowncl  6364  opelf  6782  elfvunirn  6952  fimarab  6996  fvimacnv  7086  ffvelcdm  7115  fnsnr  7199  f1imass  7301  onminex  7838  xpord2pred  8186  extmptsuppeq  8229  suppssr  8236  suppssrg  8237  dftpos3  8285  wfrlem16OLD  8380  oa00  8615  omordi  8622  omlimcl  8634  omeulem1  8638  nnmordi  8687  mapsnd  8944  ixpf  8978  pw2f1olem  9142  pssnn  9234  findcard3  9346  findcard3OLD  9347  ixpfi2  9420  fissuni  9427  elfiun  9499  dffi3  9500  ordiso2  9584  ordtypelem7  9593  ixpiunwdom  9659  inf3lem2  9698  cantnfp1lem3  9749  cantnfp1  9750  cantnflem1  9758  cantnf  9762  trcl  9797  r1ordg  9847  rankelb  9893  rankuni2b  9922  rankval4  9936  tcrank  9953  cplem1  9958  carduniima  10165  alephfp  10177  kmlem2  10221  isf32lem3  10424  domtriomlem  10511  axdc3lem2  10520  zorn2lem7  10571  ttukeylem6  10583  iundom2g  10609  fpwwe2lem12  10711  tskss  10827  tskr1om2  10837  inatsk  10847  gruss  10865  gruel  10872  grur1  10889  prlem934  11102  ltexprlem7  11111  supsr  11181  dedekind  11453  supadd  12263  supmullem2  12266  uzind  12735  iccsplit  13545  elfz0add  13683  predfz  13710  fsuppmapnn0fiub  14042  ccatval2  14626  swrdswrd  14753  pfxccatin12lem2a  14775  swrdccatin2  14777  pfxccatpfx2  14785  cshimadifsn0  14879  01sqrexlem6  15296  isercolllem2  15714  fsumcvg  15760  isumrpcl  15891  fprodcvg  15978  rpnnen2lem4  16265  fproddvdsd  16383  saddisj  16511  sadass  16517  bitsshft  16521  smuval2  16528  smupvallem  16529  smu01lem  16531  smueqlem  16536  reumodprminv  16851  ramub1lem1  17073  firest  17492  mrissmrid  17699  initoeu2lem0  18080  acsfiindd  18623  acsmapd  18624  dirge  18673  issubmnd  18799  issubg2  19181  eqgid  19220  cyccom  19243  dprdff  20056  dprddisj2  20083  ablfac1c  20115  c0rnghm  20561  issubrng2  20584  subrgdvds  20614  issubrg2  20620  rnghmsscmap  20652  rngcsect  20658  funcrngcsetc  20662  rhmsscmap  20681  rhmsscrnghm  20687  ringcsect  20692  funcringcsetc  20696  rhmsubclem4  20710  lssssr  20975  lssats2  21021  lbspss  21104  lsmelval2  21107  lspprat  21178  lbsextlem2  21184  lbsextlem3  21185  rnglidlmmgm  21278  rnglidlmsgrp  21279  rnglidlrng  21280  lpigen  21368  psgndiflemB  21641  lsmcss  21733  obselocv  21771  f1lindf  21865  issubassa3  21909  mplcoe5lem  22080  mdetdiaglem  22625  cpmadugsumlemF  22903  toprntopon  22952  elcls  23102  clsndisj  23104  elcls3  23112  neindisj  23146  lpval  23168  lpsscls  23170  lpss3  23173  maxlp  23176  restntr  23211  ordtbas2  23220  ordtbas  23221  pnfnei  23249  mnfnei  23250  cncls2  23302  lmcnp  23333  lpcls  23393  hauscmplem  23435  2ndcdisj  23485  kgen2ss  23584  txuni2  23594  ptpjpre1  23600  tx1cn  23638  tx2cn  23639  prdstopn  23657  txlm  23677  imasnopn  23719  imasncld  23720  imasncls  23721  tgqtop  23741  regr1lem  23768  fgss2  23903  uzfbas  23927  ufilmax  23936  uffix2  23953  ufildr  23960  fmfnfmlem1  23983  fmco  23990  flimrest  24012  fclsopn  24043  fclscf  24054  flimfcls  24055  alexsubALTlem4  24079  qustgplem  24150  imasf1oxms  24523  prdsbl  24525  metrest  24558  iccntr  24862  reconnlem2  24868  caucfil  25336  caussi  25350  bcthlem5  25381  ovoliunlem1  25556  shft2rab  25562  sca2rab  25566  ovolicc2  25576  vitalilem2  25663  vitalilem5  25666  mbfinf  25719  i1f1lem  25743  mbfi1fseqlem4  25773  itgss  25867  itgcn  25900  c1liplem1  26055  c1lip1  26056  c1lip3  26058  ply1remlem  26224  plyexmo  26373  taylply2  26427  lgamucov  27099  fsumvma  27275  logfaclbnd  27284  sltres  27725  nosepssdm  27749  nodenselem8  27754  nosupno  27766  nosupbday  27768  noinfbday  27783  elmade  27924  oldssmade  27934  mulsproplem13  28172  mulsproplem14  28173  precsexlem10  28258  uzsind  28409  axlowdimlem16  28990  axcontlem9  29005  edgupgr  29169  upgredg  29172  subgreldmiedg  29318  upgrres1  29348  crctcshwlkn0lem2  29844  wwlksnred  29925  clwwlkccatlem  30021  clwwlkf  30079  wwlksubclwwlk  30090  eupth2lems  30270  sspmval  30765  sspimsval  30770  ubthlem1  30902  shsubcl  31252  shorth  31327  elspansn3  31604  elnlfn  31960  elpjrn  32222  sumdmdlem2  32451  nfpconfp  32651  supssd  32723  infssd  32724  xrofsup  32774  elrspunidl  33421  ressply1mon1p  33558  cmpcref  33796  zarclsiin  33817  cntmeas  34190  1stmbfm  34225  2ndmbfm  34226  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  ballotlemimin  34470  bnj1171  34976  bnj1280  34996  subgrwlk  35100  gonarlem  35362  goalrlem  35364  mrsubrn  35481  elfzm12  35643  ontgval  36397  bj-restuni  37063  pibt2  37383  lindsenlbs  37575  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  itg2addnclem  37631  itg2addnclem2  37632  ftc1anclem7  37659  ismtyima  37763  lshpkr  39073  psubatN  39712  elpaddn0  39757  pclfinN  39857  diael  41000  dia2dimlem12  41032  dicelval1stN  41145  dicelval2nd  41146  dib2dim  41200  dih2dimbALTN  41202  dihlspsnssN  41289  dvh1dim  41399  lcfrvalsnN  41498  mapdrvallem2  41602  mapdpglem2  41630  hdmap10lem  41796  hdmap11lem2  41799  hdmapoc  41888  primrootscoprbij  42059  primrootspoweq0  42063  aks6d1c2  42087  sticksstones3  42105  sticksstones17  42120  sticksstones18  42121  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  isnacs3  42666  aomclem2  43012  kelac1  43020  rngunsnply  43130  safesnsupfiub  43378  intabssd  43481  iunrelexp0  43664  rfovcnvf1od  43966  rfovcnvfvd  43969  fsovrfovd  43971  clsk1indlem3  44005  neik0pk1imk0  44009  ntrneineine0lem  44045  ntrneiel2  44048  ntrneikb  44056  ntrneik4w  44062  mnuop3d  44240  dvconstbi  44303  expgrowth  44304  climsuselem1  45528  climsuse  45529  limcresiooub  45563  iblsplit  45887  iblspltprt  45894  stoweidlem62  45983  stirlinglem11  46005  fourierdlem41  46069  qndenserrnbllem  46215  sge0fodjrnlem  46337  smflimsuplem7  46747  fafvelcdm  47085  fafv2elcdm  47149  smonoord  47245  iccpartiltu  47296  iccpartigtl  47297  iccpartiun  47308  iccpartdisj  47311  bgoldbtbndlem2  47680  lidldomn1  47954  rhmsubcALTVlem4  48007  funcringcsetcALTV2lem9  48021  lincresunit3lem1  48208  setrec1  48783  setis  48790  vsetrec  48795  pgindnf  48808