Theorem sseld 3921

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  sselda  3922  sseldd  3923  ssneld  3924  elelpwi  4546  ssbrd  5118  uniopel  5431  exopxfr2  5756  dmrnssfld  5882  preddowncl  6239  opelf  6644  fvimacnv  6939  ffvelrn  6968  fnsnr  7046  f1imass  7146  onminex  7661  extmptsuppeq  8013  suppssr  8021  suppssrg  8022  dftpos3  8069  wfrlem16OLD  8164  oa00  8399  omordi  8406  omlimcl  8418  omeulem1  8422  nnmordi  8471  mapsnd  8683  ixpf  8717  pw2f1olem  8872  pssnn  8960  pssnnOLD  9049  findcard3  9066  ixpfi2  9126  fissuni  9133  elfiun  9198  dffi3  9199  ordiso2  9283  ordtypelem7  9292  ixpiunwdom  9358  inf3lem2  9396  cantnfp1lem3  9447  cantnfp1  9448  cantnflem1  9456  cantnf  9460  trcl  9495  r1ordg  9545  rankelb  9591  rankuni2b  9620  rankval4  9634  tcrank  9651  cplem1  9656  carduniima  9861  alephfp  9873  kmlem2  9916  isf32lem3  10120  domtriomlem  10207  axdc3lem2  10216  zorn2lem7  10267  ttukeylem6  10279  iundom2g  10305  fpwwe2lem12  10407  tskss  10523  tskr1om2  10533  inatsk  10543  gruss  10561  gruel  10568  grur1  10585  prlem934  10798  ltexprlem7  10807  supsr  10877  dedekind  11147  supadd  11952  supmullem2  11955  uzind  12421  iccsplit  13226  elfz0add  13364  predfz  13390  fsuppmapnn0fiub  13720  ccatval2  14292  swrdswrd  14427  pfxccatin12lem2a  14449  swrdccatin2  14451  pfxccatpfx2  14459  cshimadifsn0  14552  sqrlem6  14968  isercolllem2  15386  fsumcvg  15433  isumrpcl  15564  fprodcvg  15649  rpnnen2lem4  15935  fproddvdsd  16053  saddisj  16181  sadass  16187  bitsshft  16191  smuval2  16198  smupvallem  16199  smu01lem  16201  smueqlem  16206  reumodprminv  16514  ramub1lem1  16736  firest  17152  mrissmrid  17359  initoeu2lem0  17737  acsfiindd  18280  acsmapd  18281  dirge  18330  issubmnd  18421  issubg2  18779  eqgid  18817  cyccom  18831  dprdff  19624  dprddisj2  19651  ablfac1c  19683  subrgdvds  20047  issubrg2  20053  lssssr  20224  lssats2  20271  lbspss  20353  lsmelval2  20356  lspprat  20424  lbsextlem2  20430  lbsextlem3  20431  lpigen  20536  psgndiflemB  20814  lsmcss  20906  obselocv  20944  f1lindf  21038  issubassa3  21081  mplcoe5lem  21249  mdetdiaglem  21756  cpmadugsumlemF  22034  toprntopon  22083  elcls  22233  clsndisj  22235  elcls3  22243  neindisj  22277  lpval  22299  lpsscls  22301  lpss3  22304  maxlp  22307  restntr  22342  ordtbas2  22351  ordtbas  22352  pnfnei  22380  mnfnei  22381  cncls2  22433  lmcnp  22464  lpcls  22524  hauscmplem  22566  2ndcdisj  22616  kgen2ss  22715  txuni2  22725  ptpjpre1  22731  tx1cn  22769  tx2cn  22770  prdstopn  22788  txlm  22808  imasnopn  22850  imasncld  22851  imasncls  22852  tgqtop  22872  regr1lem  22899  fgss2  23034  uzfbas  23058  ufilmax  23067  uffix2  23084  ufildr  23091  fmfnfmlem1  23114  fmco  23121  flimrest  23143  fclsopn  23174  fclscf  23185  flimfcls  23186  alexsubALTlem4  23210  qustgplem  23281  imasf1oxms  23654  prdsbl  23656  metrest  23689  iccntr  23993  reconnlem2  23999  caucfil  24456  caussi  24470  bcthlem5  24501  ovoliunlem1  24675  shft2rab  24681  sca2rab  24685  ovolicc2  24695  vitalilem2  24782  vitalilem5  24785  mbfinf  24838  i1f1lem  24862  mbfi1fseqlem4  24892  itgss  24985  itgcn  25018  c1liplem1  25169  c1lip1  25170  c1lip3  25172  ply1remlem  25336  plyexmo  25482  lgamucov  26196  fsumvma  26370  logfaclbnd  26379  axlowdimlem16  27334  axcontlem9  27349  edgupgr  27513  upgredg  27516  subgreldmiedg  27659  upgrres1  27689  crctcshwlkn0lem2  28185  wwlksnred  28266  clwwlkccatlem  28362  clwwlkf  28420  wwlksubclwwlk  28431  eupth2lems  28611  sspmval  29104  sspimsval  29109  ubthlem1  29241  shsubcl  29591  shorth  29666  elspansn3  29943  elnlfn  30299  elpjrn  30561  sumdmdlem2  30790  eqrrabd  30858  nfpconfp  30976  fimarab  30989  supssd  31053  infssd  31054  xrofsup  31099  elrspunidl  31615  cmpcref  31809  zarclsiin  31830  cntmeas  32203  1stmbfm  32236  2ndmbfm  32237  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemodife  32473  ballotlemimin  32481  bnj1171  32989  bnj1280  33009  subgrwlk  33103  gonarlem  33365  goalrlem  33367  mrsubrn  33484  elfzm12  33642  xpord2pred  33801  sltres  33874  nosepssdm  33898  nodenselem8  33903  nosupno  33915  nosupbday  33917  noinfbday  33932  elmade  34060  oldssmade  34069  ontgval  34629  bj-restuni  35277  pibt2  35597  lindsenlbs  35781  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  itg2addnclem  35837  itg2addnclem2  35838  ftc1anclem7  35865  ismtyima  35970  lshpkr  37138  psubatN  37776  elpaddn0  37821  pclfinN  37921  diael  39064  dia2dimlem12  39096  dicelval1stN  39209  dicelval2nd  39210  dib2dim  39264  dih2dimbALTN  39266  dihlspsnssN  39353  dvh1dim  39463  lcfrvalsnN  39562  mapdrvallem2  39666  mapdpglem2  39694  hdmap10lem  39860  hdmap11lem2  39863  hdmapoc  39952  sticksstones3  40111  sticksstones17  40126  sticksstones18  40127  isnacs3  40539  aomclem2  40887  kelac1  40895  rngunsnply  41005  intabssd  41133  iunrelexp0  41317  rfovcnvf1od  41619  rfovcnvfvd  41622  fsovrfovd  41624  clsk1indlem3  41660  neik0pk1imk0  41664  ntrneineine0lem  41700  ntrneiel2  41703  ntrneikb  41711  ntrneik4w  41717  mnuop3d  41896  dvconstbi  41959  expgrowth  41960  climsuselem1  43155  climsuse  43156  limcresiooub  43190  iblsplit  43514  iblspltprt  43521  stoweidlem62  43610  stirlinglem11  43632  fourierdlem41  43696  qndenserrnbllem  43842  sge0fodjrnlem  43961  sssmf  44283  smflimsuplem7  44370  fafvelrn  44673  fafv2elrn  44737  smonoord  44834  iccpartiltu  44885  iccpartigtl  44886  iccpartiun  44897  iccpartdisj  44900  bgoldbtbndlem2  45269  c0rnghm  45482  lidldomn1  45490  lidlmmgm  45494  lidlmsgrp  45495  lidlrng  45496  rnghmsscmap  45543  rngcsect  45549  funcrngcsetc  45567  rhmsscmap  45589  rhmsscrnghm  45595  ringcsect  45600  funcringcsetc  45604  funcringcsetcALTV2lem9  45613  rhmsubclem4  45658  rhmsubcALTVlem4  45676  lincresunit3lem1  45831  setrec1  46408  setis  46414  vsetrec  46419