Theorem sseld 3944

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

Syntax hints:   → wi 4   ∈ wcel 2149   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-clel 2844  df-ss 3930

This theorem is referenced by:  sselda  3945  sseldd  3946  ssneld  3947  eqrrabd  4048  elelpwi  4574  ssbrd  5155  uniopel  5497  exopxfr2  5828  dmrnssfld  5962  preddowncl  6330  opelf  6737  elfvunirn  6909  fimarab  6953  fvimacnv  7046  ffvelcdm  7074  fnsnr  7159  f1imass  7260  onminex  7797  xpord2pred  8137  extmptsuppeq  8180  suppssr  8187  suppssrg  8188  dftpos3  8236  oa00  8540  omordi  8547  omlimcl  8559  omeulem1  8563  nnmordi  8613  mapsnd  8880  ixpf  8914  pw2f1olem  9065  pssnn  9149  findcard3  9239  ixpfi2  9303  fissuni  9310  elfiun  9386  dffi3  9387  supssd  9419  infssd  9450  ordiso2  9473  ordtypelem7  9482  ixpiunwdom  9548  inf3lem2  9594  cantnfp1lem3  9645  cantnfp1  9646  cantnflem1  9654  cantnf  9658  trcl  9693  r1ordg  9746  rankelb  9792  rankuni2b  9821  rankval4  9835  tcrank  9852  cplem1  9871  carduniima  10076  alephfp  10088  kmlem2  10131  isf32lem3  10335  domtriomlem  10422  axdc3lem2  10431  zorn2lem7  10482  ttukeylem6  10494  iundom2g  10520  fpwwe2lem12  10623  tskss  10739  tskr1om2  10749  inatsk  10759  gruss  10777  gruel  10784  grur1  10801  prlem934  11014  ltexprlem7  11023  supsr  11093  dedekind  11369  supadd  12179  supmullem2  12182  uzind  12684  iccsplit  13508  elfz0add  13650  predfz  13677  elfzoextl  13746  fsuppmapnn0fiub  14023  ccatval2  14611  swrdswrd  14738  pfxccatin12lem2a  14760  swrdccatin2  14762  pfxccatpfx2  14770  cshimadifsn0  14863  01sqrexlem6  15294  isercolllem2  15713  fsumcvg  15759  isumrpcl  15893  fprodcvg  15980  rpnnen2lem4  16269  fproddvdsd  16389  saddisj  16519  sadass  16525  bitsshft  16529  smuval2  16536  smupvallem  16537  smu01lem  16539  smueqlem  16544  reumodprminv  16860  ramub1lem1  17082  firest  17481  mrissmrid  17693  initoeu2lem0  18066  acsfiindd  18605  acsmapd  18606  dirge  18655  chndss  18668  issubmnd  18815  issubg2  19204  eqgid  19244  cyccom  19270  dprdff  20080  dprddisj2  20107  ablfac1c  20139  c0rnghm  20616  issubrng2  20639  subrgdvds  20667  issubrg2  20673  rnghmsscmap  20711  rngcsect  20717  funcrngcsetc  20721  rhmsscmap  20740  rhmsscrnghm  20746  ringcsect  20751  funcringcsetc  20755  rhmsubclem4  20769  lssssr  21049  lssats2  21095  lbspss  21177  lsmelval2  21180  lspprat  21251  lbsextlem2  21257  lbsextlem3  21258  rnglidlmmgm  21349  rnglidlmsgrp  21350  rnglidlrng  21351  df2idl2crng  21388  lpigen  21468  psgndiflemB  21715  lsmcss  21807  obselocv  21843  f1lindf  21937  issubassa3  21981  mplcoe5lem  22155  mdetdiaglem  22720  cpmadugsumlemF  22998  toprntopon  23047  elcls  23195  clsndisj  23197  elcls3  23205  neindisj  23239  lpval  23261  lpsscls  23263  lpss3  23266  maxlp  23269  restntr  23304  ordtbas2  23313  ordtbas  23314  pnfnei  23342  mnfnei  23343  cncls2  23395  lmcnp  23426  lpcls  23486  hauscmplem  23528  2ndcdisj  23578  kgen2ss  23677  txuni2  23687  ptpjpre1  23693  tx1cn  23731  tx2cn  23732  prdstopn  23750  txlm  23770  imasnopn  23812  imasncld  23813  imasncls  23814  tgqtop  23834  regr1lem  23861  fgss2  23996  uzfbas  24020  ufilmax  24029  uffix2  24046  ufildr  24053  fmfnfmlem1  24076  fmco  24083  flimrest  24105  fclsopn  24136  fclscf  24147  flimfcls  24148  alexsubALTlem4  24172  qustgplem  24243  imasf1oxms  24611  prdsbl  24613  metrest  24646  iccntr  24944  reconnlem2  24950  caucfil  25407  caussi  25421  bcthlem5  25452  ovoliunlem1  25626  shft2rab  25632  sca2rab  25636  ovolicc2  25646  vitalilem2  25733  vitalilem5  25736  mbfinf  25789  i1f1lem  25813  mbfi1fseqlem4  25842  itgss  25936  itgcn  25969  c1liplem1  26120  c1lip1  26121  c1lip3  26123  ply1remlem  26287  plyexmo  26439  taylply2  26493  lgamucov  27164  fsumvma  27339  logfaclbnd  27348  ltsres  27788  nosepssdm  27812  nodenselem8  27817  nosupno  27829  nosupbday  27831  noinfbday  27846  elmade  28012  oldssmade  28022  mulsproplem13  28283  mulsproplem14  28284  precsexlem10  28371  bdayons  28431  uzsind  28560  axlowdimlem16  29244  axcontlem9  29259  edgupgr  29421  upgredg  29424  subgreldmiedg  29570  upgrres1  29600  crctcshwlkn0lem2  30097  wwlksnred  30178  clwwlkccatlem  30277  clwwlkf  30335  wwlksubclwwlk  30346  eupth2lems  30526  sspmval  31022  sspimsval  31027  ubthlem1  31159  shsubcl  31509  shorth  31584  elspansn3  31861  elnlfn  32217  elpjrn  32479  sumdmdlem2  32708  nfpconfp  32914  xrofsup  33049  elrspunidl  33676  ressply1mon1p  33799  fldextrspunlsplem  34004  cmpcref  34181  zarclsiin  34202  cntmeas  34557  1stmbfm  34591  2ndmbfm  34592  ballotlemfc0  34824  ballotlemfcc  34825  ballotlemodife  34829  ballotlemimin  34837  bnj1171  35329  bnj1280  35349  r1filimi  35435  subgrwlk  35519  gonarlem  35781  goalrlem  35783  mrsubrn  35900  elfzm12  36062  ontgval  36827  elttctr  36901  bj-restuni  37622  pibt2  37946  lindsenlbs  38149  poimirlem29  38183  poimirlem30  38184  poimirlem31  38185  itg2addnclem  38205  itg2addnclem2  38206  ftc1anclem7  38233  ismtyima  38337  suceldisj  39352  lshpkr  39776  psubatN  40414  elpaddn0  40459  pclfinN  40559  diael  41702  dia2dimlem12  41734  dicelval1stN  41847  dicelval2nd  41848  dib2dim  41902  dih2dimbALTN  41904  dihlspsnssN  41991  dvh1dim  42101  lcfrvalsnN  42200  mapdrvallem2  42304  mapdpglem2  42332  hdmap10lem  42498  hdmap11lem2  42501  hdmapoc  42590  primrootscoprbij  42754  primrootspoweq0  42758  aks6d1c2  42782  sticksstones3  42800  sticksstones17  42815  sticksstones18  42816  unitscyglem2  42848  unitscyglem4  42850  unitscyglem5  42851  isnacs3  43326  aomclem2  43667  kelac1  43675  rngunsnply  43781  safesnsupfiub  44027  intabssd  44130  iunrelexp0  44313  rfovcnvf1od  44615  rfovcnvfvd  44618  fsovrfovd  44620  clsk1indlem3  44654  neik0pk1imk0  44658  ntrneineine0lem  44694  ntrneiel2  44697  ntrneikb  44705  ntrneik4w  44711  mnuop3d  44866  dvconstbi  44929  expgrowth  44930  modelaxreplem2  45573  modelaxreplem3  45574  climsuselem1  46208  climsuse  46209  limcresiooub  46241  iblsplit  46565  iblspltprt  46572  stoweidlem62  46661  stirlinglem11  46683  fourierdlem41  46747  qndenserrnbllem  46893  sge0fodjrnlem  47015  smflimsuplem7  47425  fafvelcdm  47789  fafv2elcdm  47853  ceilhalfelfzo1  47953  smonoord  47996  muldvdsfacm1  48006  iccpartiltu  48053  iccpartigtl  48054  iccpartiun  48065  iccpartdisj  48068  bgoldbtbndlem2  48453  gpgedgvtx1  48709  lidldomn1  48878  rhmsubcALTVlem4  48931  funcringcsetcALTV2lem9  48945  lincresunit3lem1  49137  setrec1  50347  setis  50354  vsetrec  50359  pgindnf  50372