Theorem sseld 3978

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

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3472  df-in 3952  df-ss 3962

This theorem is referenced by:  sselda  3979  sseldd  3980  ssneld  3981  elelpwi  4609  ssbrd  5186  uniopel  5513  exopxfr2  5842  dmrnssfld  5968  preddowncl  6333  opelf  6753  elfvunirn  6924  fvimacnv  7057  ffvelcdm  7086  fnsnr  7169  f1imass  7269  onminex  7800  xpord2pred  8145  extmptsuppeq  8187  suppssr  8195  suppssrg  8196  dftpos3  8244  wfrlem16OLD  8339  oa00  8574  omordi  8581  omlimcl  8593  omeulem1  8597  nnmordi  8646  mapsnd  8899  ixpf  8933  pw2f1olem  9095  pssnn  9187  pssnnOLD  9284  findcard3  9304  findcard3OLD  9305  ixpfi2  9369  fissuni  9376  elfiun  9448  dffi3  9449  ordiso2  9533  ordtypelem7  9542  ixpiunwdom  9608  inf3lem2  9647  cantnfp1lem3  9698  cantnfp1  9699  cantnflem1  9707  cantnf  9711  trcl  9746  r1ordg  9796  rankelb  9842  rankuni2b  9871  rankval4  9885  tcrank  9902  cplem1  9907  carduniima  10114  alephfp  10126  kmlem2  10169  isf32lem3  10373  domtriomlem  10460  axdc3lem2  10469  zorn2lem7  10520  ttukeylem6  10532  iundom2g  10558  fpwwe2lem12  10660  tskss  10776  tskr1om2  10786  inatsk  10796  gruss  10814  gruel  10821  grur1  10838  prlem934  11051  ltexprlem7  11060  supsr  11130  dedekind  11402  supadd  12207  supmullem2  12210  uzind  12679  iccsplit  13489  elfz0add  13627  predfz  13653  fsuppmapnn0fiub  13983  ccatval2  14555  swrdswrd  14682  pfxccatin12lem2a  14704  swrdccatin2  14706  pfxccatpfx2  14714  cshimadifsn0  14808  01sqrexlem6  15221  isercolllem2  15639  fsumcvg  15685  isumrpcl  15816  fprodcvg  15901  rpnnen2lem4  16188  fproddvdsd  16306  saddisj  16434  sadass  16440  bitsshft  16444  smuval2  16451  smupvallem  16452  smu01lem  16454  smueqlem  16459  reumodprminv  16767  ramub1lem1  16989  firest  17408  mrissmrid  17615  initoeu2lem0  17996  acsfiindd  18539  acsmapd  18540  dirge  18589  issubmnd  18715  issubg2  19090  eqgid  19129  cyccom  19152  dprdff  19963  dprddisj2  19990  ablfac1c  20022  c0rnghm  20466  issubrng2  20489  subrgdvds  20519  issubrg2  20525  rnghmsscmap  20557  rngcsect  20563  funcrngcsetc  20567  rhmsscmap  20586  rhmsscrnghm  20592  ringcsect  20597  funcringcsetc  20601  rhmsubclem4  20615  lssssr  20832  lssats2  20878  lbspss  20961  lsmelval2  20964  lspprat  21035  lbsextlem2  21041  lbsextlem3  21042  rnglidlmmgm  21134  rnglidlmsgrp  21135  rnglidlrng  21136  lpigen  21219  psgndiflemB  21526  lsmcss  21618  obselocv  21656  f1lindf  21750  issubassa3  21793  mplcoe5lem  21971  mdetdiaglem  22494  cpmadugsumlemF  22772  toprntopon  22821  elcls  22971  clsndisj  22973  elcls3  22981  neindisj  23015  lpval  23037  lpsscls  23039  lpss3  23042  maxlp  23045  restntr  23080  ordtbas2  23089  ordtbas  23090  pnfnei  23118  mnfnei  23119  cncls2  23171  lmcnp  23202  lpcls  23262  hauscmplem  23304  2ndcdisj  23354  kgen2ss  23453  txuni2  23463  ptpjpre1  23469  tx1cn  23507  tx2cn  23508  prdstopn  23526  txlm  23546  imasnopn  23588  imasncld  23589  imasncls  23590  tgqtop  23610  regr1lem  23637  fgss2  23772  uzfbas  23796  ufilmax  23805  uffix2  23822  ufildr  23829  fmfnfmlem1  23852  fmco  23859  flimrest  23881  fclsopn  23912  fclscf  23923  flimfcls  23924  alexsubALTlem4  23948  qustgplem  24019  imasf1oxms  24392  prdsbl  24394  metrest  24427  iccntr  24731  reconnlem2  24737  caucfil  25205  caussi  25219  bcthlem5  25250  ovoliunlem1  25425  shft2rab  25431  sca2rab  25435  ovolicc2  25445  vitalilem2  25532  vitalilem5  25535  mbfinf  25588  i1f1lem  25612  mbfi1fseqlem4  25642  itgss  25735  itgcn  25768  c1liplem1  25923  c1lip1  25924  c1lip3  25926  ply1remlem  26093  plyexmo  26242  taylply2  26296  lgamucov  26964  fsumvma  27140  logfaclbnd  27149  sltres  27589  nosepssdm  27613  nodenselem8  27618  nosupno  27630  nosupbday  27632  noinfbday  27647  elmade  27788  oldssmade  27798  mulsproplem13  28022  mulsproplem14  28023  precsexlem10  28108  axlowdimlem16  28762  axcontlem9  28777  edgupgr  28941  upgredg  28944  subgreldmiedg  29090  upgrres1  29120  crctcshwlkn0lem2  29616  wwlksnred  29697  clwwlkccatlem  29793  clwwlkf  29851  wwlksubclwwlk  29862  eupth2lems  30042  sspmval  30537  sspimsval  30542  ubthlem1  30674  shsubcl  31024  shorth  31099  elspansn3  31376  elnlfn  31732  elpjrn  31994  sumdmdlem2  32223  eqrrabd  32293  nfpconfp  32411  fimarab  32423  supssd  32486  infssd  32487  xrofsup  32532  elrspunidl  33139  ressply1mon1p  33238  cmpcref  33446  zarclsiin  33467  cntmeas  33840  1stmbfm  33875  2ndmbfm  33876  ballotlemfc0  34107  ballotlemfcc  34108  ballotlemodife  34112  ballotlemimin  34120  bnj1171  34626  bnj1280  34646  subgrwlk  34737  gonarlem  34999  goalrlem  35001  mrsubrn  35118  elfzm12  35274  ontgval  35910  bj-restuni  36571  pibt2  36891  lindsenlbs  37083  poimirlem29  37117  poimirlem30  37118  poimirlem31  37119  itg2addnclem  37139  itg2addnclem2  37140  ftc1anclem7  37167  ismtyima  37271  lshpkr  38584  psubatN  39223  elpaddn0  39268  pclfinN  39368  diael  40511  dia2dimlem12  40543  dicelval1stN  40656  dicelval2nd  40657  dib2dim  40711  dih2dimbALTN  40713  dihlspsnssN  40800  dvh1dim  40910  lcfrvalsnN  41009  mapdrvallem2  41113  mapdpglem2  41141  hdmap10lem  41307  hdmap11lem2  41310  hdmapoc  41399  primrootscoprbij  41568  primrootspoweq0  41572  aks6d1c2  41596  sticksstones3  41615  sticksstones17  41630  sticksstones18  41631  isnacs3  42121  aomclem2  42470  kelac1  42478  rngunsnply  42588  safesnsupfiub  42837  intabssd  42940  iunrelexp0  43123  rfovcnvf1od  43425  rfovcnvfvd  43428  fsovrfovd  43430  clsk1indlem3  43464  neik0pk1imk0  43468  ntrneineine0lem  43504  ntrneiel2  43507  ntrneikb  43515  ntrneik4w  43521  mnuop3d  43699  dvconstbi  43762  expgrowth  43763  climsuselem1  44986  climsuse  44987  limcresiooub  45021  iblsplit  45345  iblspltprt  45352  stoweidlem62  45441  stirlinglem11  45463  fourierdlem41  45527  qndenserrnbllem  45673  sge0fodjrnlem  45795  sssmf  46117  smflimsuplem7  46205  fafvelcdm  46541  fafv2elcdm  46605  smonoord  46702  iccpartiltu  46753  iccpartigtl  46754  iccpartiun  46765  iccpartdisj  46768  bgoldbtbndlem2  47137  lidldomn1  47284  rhmsubcALTVlem4  47337  funcringcsetcALTV2lem9  47351  lincresunit3lem1  47538  setrec1  48113  setis  48120  vsetrec  48125  pgindnf  48138