Theorem sseld 3925

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3892

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  sselda  3926  sseldd  3927  ssneld  3928  elelpwi  4551  ssbrd  5122  uniopel  5434  exopxfr2  5752  dmrnssfld  5878  preddowncl  6234  opelf  6633  fvimacnv  6927  ffvelrn  6956  fnsnr  7034  f1imass  7134  onminex  7647  extmptsuppeq  7996  suppssr  8004  suppssrg  8005  dftpos3  8052  wfrlem16OLD  8147  oa00  8382  omordi  8389  omlimcl  8401  omeulem1  8405  nnmordi  8454  mapsnd  8666  ixpf  8700  pw2f1olem  8854  pssnn  8942  pssnnOLD  9028  findcard3  9045  ixpfi2  9105  fissuni  9112  elfiun  9177  dffi3  9178  ordiso2  9262  ordtypelem7  9271  ixpiunwdom  9337  inf3lem2  9375  cantnfp1lem3  9426  cantnfp1  9427  cantnflem1  9435  cantnf  9439  trpredtr  9487  trpredmintr  9488  dftrpred3g  9491  trpredrec  9494  trcl  9496  r1ordg  9547  rankelb  9593  rankuni2b  9622  rankval4  9636  tcrank  9653  cplem1  9658  carduniima  9863  alephfp  9875  kmlem2  9918  isf32lem3  10122  domtriomlem  10209  axdc3lem2  10218  zorn2lem7  10269  ttukeylem6  10281  iundom2g  10307  fpwwe2lem12  10409  tskss  10525  tskr1om2  10535  inatsk  10545  gruss  10563  gruel  10570  grur1  10587  prlem934  10800  ltexprlem7  10809  supsr  10879  dedekind  11149  supadd  11954  supmullem2  11957  uzind  12423  iccsplit  13228  elfz0add  13366  predfz  13392  fsuppmapnn0fiub  13722  ccatval2  14294  swrdswrd  14429  pfxccatin12lem2a  14451  swrdccatin2  14453  pfxccatpfx2  14461  cshimadifsn0  14554  sqrlem6  14970  isercolllem2  15388  fsumcvg  15435  isumrpcl  15566  fprodcvg  15651  rpnnen2lem4  15937  fproddvdsd  16055  saddisj  16183  sadass  16189  bitsshft  16193  smuval2  16200  smupvallem  16201  smu01lem  16203  smueqlem  16208  reumodprminv  16516  ramub1lem1  16738  firest  17154  mrissmrid  17361  initoeu2lem0  17739  acsfiindd  18282  acsmapd  18283  dirge  18332  issubmnd  18423  issubg2  18781  eqgid  18819  cyccom  18833  dprdff  19626  dprddisj2  19653  ablfac1c  19685  subrgdvds  20049  issubrg2  20055  lssssr  20226  lssats2  20273  lbspss  20355  lsmelval2  20358  lspprat  20426  lbsextlem2  20432  lbsextlem3  20433  lpigen  20538  psgndiflemB  20816  lsmcss  20908  obselocv  20946  f1lindf  21040  issubassa3  21083  mplcoe5lem  21251  mdetdiaglem  21758  cpmadugsumlemF  22036  toprntopon  22085  elcls  22235  clsndisj  22237  elcls3  22245  neindisj  22279  lpval  22301  lpsscls  22303  lpss3  22306  maxlp  22309  restntr  22344  ordtbas2  22353  ordtbas  22354  pnfnei  22382  mnfnei  22383  cncls2  22435  lmcnp  22466  lpcls  22526  hauscmplem  22568  2ndcdisj  22618  kgen2ss  22717  txuni2  22727  ptpjpre1  22733  tx1cn  22771  tx2cn  22772  prdstopn  22790  txlm  22810  imasnopn  22852  imasncld  22853  imasncls  22854  tgqtop  22874  regr1lem  22901  fgss2  23036  uzfbas  23060  ufilmax  23069  uffix2  23086  ufildr  23093  fmfnfmlem1  23116  fmco  23123  flimrest  23145  fclsopn  23176  fclscf  23187  flimfcls  23188  alexsubALTlem4  23212  qustgplem  23283  imasf1oxms  23656  prdsbl  23658  metrest  23691  iccntr  23995  reconnlem2  24001  caucfil  24458  caussi  24472  bcthlem5  24503  ovoliunlem1  24677  shft2rab  24683  sca2rab  24687  ovolicc2  24697  vitalilem2  24784  vitalilem5  24787  mbfinf  24840  i1f1lem  24864  mbfi1fseqlem4  24894  itgss  24987  itgcn  25020  c1liplem1  25171  c1lip1  25172  c1lip3  25174  ply1remlem  25338  plyexmo  25484  lgamucov  26198  fsumvma  26372  logfaclbnd  26381  axlowdimlem16  27336  axcontlem9  27351  edgupgr  27515  upgredg  27518  subgreldmiedg  27661  upgrres1  27691  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  37140  psubatN  37778  elpaddn0  37823  pclfinN  37923  diael  39066  dia2dimlem12  39098  dicelval1stN  39211  dicelval2nd  39212  dib2dim  39266  dih2dimbALTN  39268  dihlspsnssN  39355  dvh1dim  39465  lcfrvalsnN  39564  mapdrvallem2  39668  mapdpglem2  39696  hdmap10lem  39862  hdmap11lem2  39865  hdmapoc  39954  sticksstones3  40113  sticksstones17  40128  sticksstones18  40129  isnacs3  40541  aomclem2  40889  kelac1  40897  rngunsnply  41007  intabssd  41117  iunrelexp0  41292  rfovcnvf1od  41594  rfovcnvfvd  41597  fsovrfovd  41599  clsk1indlem3  41635  neik0pk1imk0  41639  ntrneineine0lem  41675  ntrneiel2  41678  ntrneikb  41686  ntrneik4w  41692  mnuop3d  41871  dvconstbi  41934  expgrowth  41935  climsuselem1  43130  climsuse  43131  limcresiooub  43165  iblsplit  43489  iblspltprt  43496  stoweidlem62  43585  stirlinglem11  43607  fourierdlem41  43671  qndenserrnbllem  43817  sge0fodjrnlem  43936  sssmf  44253  smflimsuplem7  44338  fafvelrn  44641  fafv2elrn  44705  smonoord  44802  iccpartiltu  44853  iccpartigtl  44854  iccpartiun  44865  iccpartdisj  44868  bgoldbtbndlem2  45237  c0rnghm  45450  lidldomn1  45458  lidlmmgm  45462  lidlmsgrp  45463  lidlrng  45464  rnghmsscmap  45511  rngcsect  45517  funcrngcsetc  45535  rhmsscmap  45557  rhmsscrnghm  45563  ringcsect  45568  funcringcsetc  45572  funcringcsetcALTV2lem9  45581  rhmsubclem4  45626  rhmsubcALTVlem4  45644  lincresunit3lem1  45799  setrec1  46376  setis  46382  vsetrec  46387