Theorem sseld 3968

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  sselda  3969  sseldd  3970  ssneld  3971  elelpwi  4553  ssbrd  5111  uniopel  5408  exopxfr2  5717  dmrnssfld  5843  preddowncl  6177  opelf  6541  fvimacnv  6825  ffvelrn  6851  fnsnr  6929  f1imass  7024  onminex  7524  extmptsuppeq  7856  suppssr  7863  dftpos3  7912  wfrlem16  7972  oa00  8187  omordi  8194  omlimcl  8206  omeulem1  8210  nnmordi  8259  mapsnd  8452  ixpf  8486  pw2f1olem  8623  pssnn  8738  findcard3  8763  ixpfi2  8824  fissuni  8831  elfiun  8896  dffi3  8897  ordiso2  8981  ordtypelem7  8990  ixpiunwdom  9057  inf3lem2  9094  cantnfp1lem3  9145  cantnfp1  9146  cantnflem1  9154  cantnf  9158  trcl  9172  r1ordg  9209  rankelb  9255  rankuni2b  9284  rankval4  9298  tcrank  9315  cplem1  9320  carduniima  9524  alephfp  9536  kmlem2  9579  isf32lem3  9779  domtriomlem  9866  axdc3lem2  9875  zorn2lem7  9926  ttukeylem6  9938  iundom2g  9964  fpwwe2lem13  10066  tskss  10182  tskr1om2  10192  inatsk  10202  gruss  10220  gruel  10227  grur1  10244  prlem934  10457  ltexprlem7  10466  supsr  10536  dedekind  10805  supadd  11611  supmullem2  11614  uzind  12077  iccsplit  12874  elfz0add  13009  predfz  13035  fsuppmapnn0fiub  13362  ccatval2  13934  swrdswrd  14069  pfxccatin12lem2a  14091  swrdccatin2  14093  pfxccatpfx2  14101  cshimadifsn0  14194  sqrlem6  14609  isercolllem2  15024  fsumcvg  15071  isumrpcl  15200  fprodcvg  15286  rpnnen2lem4  15572  fproddvdsd  15686  saddisj  15816  sadass  15822  bitsshft  15826  smuval2  15833  smupvallem  15834  smu01lem  15836  smueqlem  15841  reumodprminv  16143  ramub1lem1  16364  firest  16708  mrissmrid  16914  initoeu2lem0  17275  acsfiindd  17789  acsmapd  17790  dirge  17849  issubmnd  17940  issubg2  18296  eqgid  18334  cyccom  18348  dprdff  19136  dprddisj2  19163  ablfac1c  19195  subrgdvds  19551  issubrg2  19557  lssssr  19727  lssats2  19774  lbspss  19856  lsmelval2  19859  lspprat  19927  lbsextlem2  19933  lbsextlem3  19934  lpigen  20031  issubassa3  20099  mplcoe5lem  20250  psgndiflemB  20746  lsmcss  20838  obselocv  20874  f1lindf  20968  mdetdiaglem  21209  cpmadugsumlemF  21486  toprntopon  21535  elcls  21683  clsndisj  21685  elcls3  21693  neindisj  21727  lpval  21749  lpsscls  21751  lpss3  21754  maxlp  21757  restntr  21792  ordtbas2  21801  ordtbas  21802  pnfnei  21830  mnfnei  21831  cncls2  21883  lmcnp  21914  lpcls  21974  hauscmplem  22016  2ndcdisj  22066  kgen2ss  22165  txuni2  22175  ptpjpre1  22181  tx1cn  22219  tx2cn  22220  prdstopn  22238  txlm  22258  imasnopn  22300  imasncld  22301  imasncls  22302  tgqtop  22322  regr1lem  22349  fgss2  22484  uzfbas  22508  ufilmax  22517  uffix2  22534  ufildr  22541  fmfnfmlem1  22564  fmco  22571  flimrest  22593  fclsopn  22624  fclscf  22635  flimfcls  22636  alexsubALTlem4  22660  qustgplem  22731  imasf1oxms  23101  prdsbl  23103  metrest  23136  iccntr  23431  reconnlem2  23437  caucfil  23888  caussi  23902  bcthlem5  23933  ovoliunlem1  24105  shft2rab  24111  sca2rab  24115  ovolicc2  24125  vitalilem2  24212  vitalilem5  24215  mbfinf  24268  i1f1lem  24292  mbfi1fseqlem4  24321  itgss  24414  itgcn  24445  c1liplem1  24595  c1lip1  24596  c1lip3  24598  ply1remlem  24758  plyexmo  24904  lgamucov  25617  fsumvma  25791  logfaclbnd  25800  axlowdimlem16  26745  axcontlem9  26760  edgupgr  26921  upgredg  26924  subgreldmiedg  27067  upgrres1  27097  crctcshwlkn0lem2  27591  wwlksnred  27672  clwwlkccatlem  27769  clwwlkf  27828  wwlksubclwwlk  27839  eupth2lems  28019  sspmval  28512  sspimsval  28517  ubthlem1  28649  shsubcl  28999  shorth  29074  elspansn3  29351  elnlfn  29707  elpjrn  29969  sumdmdlem2  30198  nfpconfp  30379  fimarab  30392  supssd  30447  infssd  30448  xrofsup  30494  cmpcref  31116  cntmeas  31487  1stmbfm  31520  2ndmbfm  31521  ballotlemfc0  31752  ballotlemfcc  31753  ballotlemodife  31757  ballotlemimin  31765  bnj1171  32274  bnj1280  32294  subgrwlk  32381  gonarlem  32643  goalrlem  32645  mrsubrn  32762  elfzm12  32920  trpredtr  33071  trpredmintr  33072  dftrpred3g  33074  trpredrec  33079  sltres  33171  nosepssdm  33192  nodenselem8  33197  nosupno  33205  nosupbday  33207  ontgval  33781  bj-restuni  34390  pibt2  34700  lindsenlbs  34889  poimirlem16  34910  poimirlem29  34923  poimirlem30  34924  poimirlem31  34925  itg2addnclem  34945  itg2addnclem2  34946  ftc1anclem7  34975  ismtyima  35083  lshpkr  36255  psubatN  36893  elpaddn0  36938  pclfinN  37038  diael  38181  dia2dimlem12  38213  dicelval1stN  38326  dicelval2nd  38327  dib2dim  38381  dih2dimbALTN  38383  dihlspsnssN  38470  dvh1dim  38580  lcfrvalsnN  38679  mapdrvallem2  38783  mapdpglem2  38811  hdmap10lem  38977  hdmap11lem2  38980  hdmapoc  39069  isnacs3  39314  aomclem2  39662  kelac1  39670  rngunsnply  39780  intabssd  39892  iunrelexp0  40054  rfovcnvf1od  40357  rfovcnvfvd  40360  fsovrfovd  40362  clsk1indlem3  40400  neik0pk1imk0  40404  ntrneineine0lem  40440  ntrneiel2  40443  ntrneikb  40451  ntrneik4w  40457  mnuop3d  40614  dvconstbi  40673  expgrowth  40674  climsuselem1  41895  climsuse  41896  limcresiooub  41930  iblsplit  42258  iblspltprt  42265  stoweidlem62  42354  stirlinglem11  42376  fourierdlem41  42440  qndenserrnbllem  42586  sge0fodjrnlem  42705  sssmf  43022  smflimsuplem7  43107  fafvelrn  43376  fafv2elrn  43440  smonoord  43538  iccpartiltu  43589  iccpartigtl  43590  iccpartiun  43601  iccpartdisj  43604  bgoldbtbndlem2  43978  c0rnghm  44191  lidldomn1  44199  lidlmmgm  44203  lidlmsgrp  44204  lidlrng  44205  rnghmsscmap  44252  rngcsect  44258  funcrngcsetc  44276  rhmsscmap  44298  rhmsscrnghm  44304  ringcsect  44309  funcringcsetc  44313  funcringcsetcALTV2lem9  44322  rhmsubclem4  44367  rhmsubcALTVlem4  44385  lincresunit3lem1  44541  setrec1  44801  setis  44807  vsetrec  44812