Theorem sseld 3912

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2839  df-ss 3901

This theorem is used by:  sselda  3913  sseldd  3914  ssneld  3915  eqrrabd  4014  elelpwi  4570  ssbrd  5154  uniopel  5496  exopxfr2  5832  dmrnssfld  5968  preddowncl  6361  opelf  6773  elfvunirn  6946  fimarab  6990  fvimacnv  7083  ffvelcdm  7113  fnsnr  7200  f1imass  7299  onminex  7850  xpord2pred  8199  extmptsuppeq  8243  suppssr  8250  suppssrg  8251  dftpos3  8299  oa00  8605  omordi  8612  omlimcl  8624  omeulem1  8628  nnmordi  8678  mapsnd  8952  ixpf  8986  pw2f1olem  9138  pssnn  9222  findcard3  9312  ixpfi2  9377  fissuni  9384  elfiun  9459  dffi3  9460  supssd  9492  infssd  9523  ordiso2  9546  ordtypelem7  9555  ixpiunwdom  9621  inf3lem2  9667  cantnfp1lem3  9718  cantnfp1  9719  cantnflem1  9727  cantnf  9731  trcl  9766  r1ordg  9822  rankelb  9870  rankuni2b  9904  rankval4  9921  tcrank  9938  r1filimi  9940  cplem1  9987  cplem1OLD  9988  setrec1  10009  carduniima  10214  alephfp  10226  kmlem2  10269  isf32lem3  10472  domtriomlem  10559  axdc3lem2  10568  zorn2lem7  10619  ttukeylem6  10631  iundom2g  10663  fpwwe2lem12  10766  tskss  10882  tskhf  10892  inatsk  10902  gruss  10920  gruel  10927  grur1  10944  prlem934  11157  ltexprlem7  11166  supsr  11236  dedekind  11512  supadd  12325  supmullem2  12328  uzind  12831  iccsplit  13656  elfz0add  13800  predfz  13827  elfzoextl  13896  fsuppmapnn0fiub  14174  ccatval2  14764  swrdswrd  14896  pfxccatin12lem2a  14918  swrdccatin2  14920  pfxccatpfx2  14928  cshimadifsn0  15023  01sqrexlem6  15457  isercolllem2  15877  fsumcvg  15922  isumrpcl  16056  fprodcvg  16141  rpnnen2lem4  16429  fproddvdsd  16549  saddisj  16679  sadass  16685  bitsshft  16689  smuval2  16696  smupvallem  16697  smu01lem  16699  smueqlem  16704  reumodprminv  17026  ramub1lem1  17248  firest  17653  mrissmrid  17865  initoeu2lem0  18238  acsfiindd  18777  acsmapd  18778  dirge  18827  chndss  18840  issubmnd  19003  issubg2  19402  eqgid  19442  cyccom  19468  dprdff  20279  dprddisj2  20306  ablfac1c  20338  c0rnghm  20838  issubrng2  20861  subrgdvds  20889  issubrg2  20895  rnghmsscmap  20933  rngcsect  20939  funcrngcsetc  20943  rhmsscmap  20962  rhmsscrnghm  20968  ringcsect  20973  funcringcsetc  20977  rhmsubclem4  20991  lssssr  21280  lssats2  21326  lbspss  21408  lsmelval2  21411  lspprat  21482  lbsextlem2  21488  lbsextlem3  21489  rnglidlmmgm  21584  rnglidlmsgrp  21585  rnglidlrng  21586  df2idl2crng  21628  lpigen  21710  psgndiflemB  21961  lsmcss  22053  obselocv  22089  f1lindf  22183  lindsenlbs  22212  issubassa3  22229  mplcoe5lem  22403  mdetdiaglem  22968  cpmadugsumlemF  23249  toprntopon  23298  elcls  23446  clsndisj  23448  elcls3  23456  neindisj  23490  lpval  23512  lpsscls  23514  lpss3  23517  maxlp  23520  restntr  23555  ordtbas2  23564  ordtbas  23565  pnfnei  23593  mnfnei  23594  cncls2  23646  lmcnp  23677  lpcls  23737  hauscmplem  23779  2ndcdisj  23830  kgen2ss  23929  txuni2  23939  ptpjpre1  23945  tx1cn  23983  tx2cn  23984  prdstopn  24002  txlm  24022  imasnopn  24064  imasncld  24065  imasncls  24066  tgqtop  24086  regr1lem  24113  fgss2  24248  uzfbas  24272  ufilmax  24281  uffix2  24298  ufildr  24305  fmfnfmlem1  24328  fmco  24335  flimrest  24357  fclsopn  24388  fclscf  24399  flimfcls  24400  alexsubALTlem4  24424  qustgplem  24495  imasf1oxms  24863  prdsbl  24865  metrest  24898  iccntr  25196  reconnlem2  25202  caucfil  25659  caussi  25673  bcthlem5  25704  ovoliunlem1  25878  shft2rab  25884  sca2rab  25888  ovolicc2  25898  vitalilem2  25985  vitalilem5  25988  mbfinf  26041  i1f1lem  26065  mbfi1fseqlem4  26094  itgss  26187  itgcn  26220  c1liplem1  26371  c1lip1  26372  c1lip3  26374  ply1remlem  26538  plyconz  26686  plyexmo  26691  rngunsnply  26693  taylply2  26752  lgamucov  27422  fsumvma  27597  logfaclbnd  27606  ltsres  28076  nosepssdm  28100  nodenselem8  28105  nosupno  28117  nosupbday  28119  noinfbday  28134  elmade  28300  oldssmade  28310  mulsproplem13  28571  mulsproplem14  28572  precsexlem10  28659  bdayons  28719  uzsind  28848  axlowdimlem16  29592  axcontlem9  29607  edgupgr  29769  upgredg  29772  subgreldmiedg  29921  upgrres1  29951  subgrwlk  30326  crctcshwlkn0lem2  30457  wwlksnred  30538  clwwlkccatlem  30637  clwwlkf  30695  wwlksubclwwlk  30706  eupth2lems  30896  sspmval  31392  sspimsval  31397  ubthlem1  31529  shsubcl  31879  shorth  31954  elspansn3  32231  elnlfn  32587  elpjrn  32849  sumdmdlem2  33078  nfpconfp  33324  xrofsup  33455  elrspunidl  34082  ressply1mon1p  34203  rngunsnply1  34249  fldextrspunlsplem  34416  cmpcref  34593  zarclsiin  34614  cntmeas  34970  1stmbfm  35003  2ndmbfm  35004  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemodife  35241  ballotlemimin  35249  bnj1171  35741  bnj1280  35761  ptpconn  36206  gonarlem  36367  goalrlem  36369  mrsubrn  36486  elfzm12  36648  elpssmo  36673  ontgval  37434  elttctr  37508  bj-restuni  38288  pibt2  38608  poimirlem29  38835  poimirlem30  38836  poimirlem31  38837  itg2addnclem  38857  itg2addnclem2  38858  ftc1anclem7  38885  ismtyima  39003  suceldisj  40016  lshpkr  40440  psubatN  41078  elpaddn0  41123  pclfinN  41223  diael  42366  dia2dimlem12  42398  dicelval1stN  42511  dicelval2nd  42512  dib2dim  42566  dih2dimbALTN  42568  dihlspsnssN  42655  dvh1dim  42765  lcfrvalsnN  42864  mapdrvallem2  42968  mapdpglem2  42996  hdmap10lem  43162  hdmap11lem2  43165  hdmapoc  43254  primrootscoprbij  43418  primrootspoweq0  43422  aks6d1c2  43446  sticksstones3  43464  sticksstones17  43479  sticksstones18  43480  unitscyglem2  43512  unitscyglem4  43514  unitscyglem5  43515  isnacs3  43987  aomclem2  44323  kelac1  44331  safesnsupfiub  44678  intabssd  44781  iunrelexp0  44963  rfovcnvf1od  45265  rfovcnvfvd  45268  fsovrfovd  45270  clsk1indlem3  45304  neik0pk1imk0  45308  ntrneineine0lem  45344  ntrneiel2  45347  ntrneikb  45355  ntrneik4w  45361  mnuop3d  45516  dvconstbi  45579  expgrowth  45580  cocanss2  46183  modelaxreplem2  46233  modelaxreplem3  46234  climsuselem1  46892  climsuse  46893  limcresiooub  46925  iblsplit  47249  iblspltprt  47256  stoweidlem62  47345  stirlinglem11  47367  fourierdlem41  47431  qndenserrnbllem  47577  sge0fodjrnlem  47699  smflimsuplem7  48109  fafvelcdm  48513  fafv2elcdm  48577  ceilhalfelfzo1  48677  smonoord  48720  muldvdsfacm1  48730  iccpartiltu  48777  iccpartigtl  48778  iccpartiun  48789  iccpartdisj  48792  bgoldbtbndlem2  49177  gpgedgvtx1  49433  lidldomn1  49601  rhmsubcALTVlem4  49654  funcringcsetcALTV2lem9  49668  lincresunit3lem1  49922  setis  51197  vsetrec  51202  pgindnf  51215