Theorem sseld 3981

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

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

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965

This theorem is referenced by:  sselda  3982  sseldd  3983  ssneld  3984  elelpwi  4612  ssbrd  5191  uniopel  5516  exopxfr2  5843  dmrnssfld  5968  preddowncl  6331  opelf  6750  elfvunirn  6921  fvimacnv  7052  ffvelcdm  7081  fnsnr  7160  f1imass  7260  onminex  7787  xpord2pred  8128  extmptsuppeq  8170  suppssr  8178  suppssrg  8179  dftpos3  8226  wfrlem16OLD  8321  oa00  8556  omordi  8563  omlimcl  8575  omeulem1  8579  nnmordi  8628  mapsnd  8877  ixpf  8911  pw2f1olem  9073  pssnn  9165  pssnnOLD  9262  findcard3  9282  findcard3OLD  9283  ixpfi2  9347  fissuni  9354  elfiun  9422  dffi3  9423  ordiso2  9507  ordtypelem7  9516  ixpiunwdom  9582  inf3lem2  9621  cantnfp1lem3  9672  cantnfp1  9673  cantnflem1  9681  cantnf  9685  trcl  9720  r1ordg  9770  rankelb  9816  rankuni2b  9845  rankval4  9859  tcrank  9876  cplem1  9881  carduniima  10088  alephfp  10100  kmlem2  10143  isf32lem3  10347  domtriomlem  10434  axdc3lem2  10443  zorn2lem7  10494  ttukeylem6  10506  iundom2g  10532  fpwwe2lem12  10634  tskss  10750  tskr1om2  10760  inatsk  10770  gruss  10788  gruel  10795  grur1  10812  prlem934  11025  ltexprlem7  11034  supsr  11104  dedekind  11374  supadd  12179  supmullem2  12182  uzind  12651  iccsplit  13459  elfz0add  13597  predfz  13623  fsuppmapnn0fiub  13953  ccatval2  14525  swrdswrd  14652  pfxccatin12lem2a  14674  swrdccatin2  14676  pfxccatpfx2  14684  cshimadifsn0  14778  01sqrexlem6  15191  isercolllem2  15609  fsumcvg  15655  isumrpcl  15786  fprodcvg  15871  rpnnen2lem4  16157  fproddvdsd  16275  saddisj  16403  sadass  16409  bitsshft  16413  smuval2  16420  smupvallem  16421  smu01lem  16423  smueqlem  16428  reumodprminv  16734  ramub1lem1  16956  firest  17375  mrissmrid  17582  initoeu2lem0  17960  acsfiindd  18503  acsmapd  18504  dirge  18553  issubmnd  18649  issubg2  19016  eqgid  19055  cyccom  19075  dprdff  19877  dprddisj2  19904  ablfac1c  19936  subrgdvds  20370  issubrg2  20376  lssssr  20557  lssats2  20604  lbspss  20686  lsmelval2  20689  lspprat  20759  lbsextlem2  20765  lbsextlem3  20766  lpigen  20887  psgndiflemB  21145  lsmcss  21237  obselocv  21275  f1lindf  21369  issubassa3  21412  mplcoe5lem  21586  mdetdiaglem  22092  cpmadugsumlemF  22370  toprntopon  22419  elcls  22569  clsndisj  22571  elcls3  22579  neindisj  22613  lpval  22635  lpsscls  22637  lpss3  22640  maxlp  22643  restntr  22678  ordtbas2  22687  ordtbas  22688  pnfnei  22716  mnfnei  22717  cncls2  22769  lmcnp  22800  lpcls  22860  hauscmplem  22902  2ndcdisj  22952  kgen2ss  23051  txuni2  23061  ptpjpre1  23067  tx1cn  23105  tx2cn  23106  prdstopn  23124  txlm  23144  imasnopn  23186  imasncld  23187  imasncls  23188  tgqtop  23208  regr1lem  23235  fgss2  23370  uzfbas  23394  ufilmax  23403  uffix2  23420  ufildr  23427  fmfnfmlem1  23450  fmco  23457  flimrest  23479  fclsopn  23510  fclscf  23521  flimfcls  23522  alexsubALTlem4  23546  qustgplem  23617  imasf1oxms  23990  prdsbl  23992  metrest  24025  iccntr  24329  reconnlem2  24335  caucfil  24792  caussi  24806  bcthlem5  24837  ovoliunlem1  25011  shft2rab  25017  sca2rab  25021  ovolicc2  25031  vitalilem2  25118  vitalilem5  25121  mbfinf  25174  i1f1lem  25198  mbfi1fseqlem4  25228  itgss  25321  itgcn  25354  c1liplem1  25505  c1lip1  25506  c1lip3  25508  ply1remlem  25672  plyexmo  25818  lgamucov  26532  fsumvma  26706  logfaclbnd  26715  sltres  27155  nosepssdm  27179  nodenselem8  27184  nosupno  27196  nosupbday  27198  noinfbday  27213  elmade  27352  oldssmade  27362  mulsproplem13  27574  mulsproplem14  27575  precsexlem10  27652  axlowdimlem16  28205  axcontlem9  28220  edgupgr  28384  upgredg  28387  subgreldmiedg  28530  upgrres1  28560  crctcshwlkn0lem2  29055  wwlksnred  29136  clwwlkccatlem  29232  clwwlkf  29290  wwlksubclwwlk  29301  eupth2lems  29481  sspmval  29974  sspimsval  29979  ubthlem1  30111  shsubcl  30461  shorth  30536  elspansn3  30813  elnlfn  31169  elpjrn  31431  sumdmdlem2  31660  eqrrabd  31729  nfpconfp  31844  fimarab  31856  supssd  31922  infssd  31923  xrofsup  31968  elrspunidl  32535  ressply1mon1p  32646  cmpcref  32819  zarclsiin  32840  cntmeas  33213  1stmbfm  33248  2ndmbfm  33249  ballotlemfc0  33480  ballotlemfcc  33481  ballotlemodife  33485  ballotlemimin  33493  bnj1171  34000  bnj1280  34020  subgrwlk  34112  gonarlem  34374  goalrlem  34376  mrsubrn  34493  elfzm12  34649  ontgval  35305  bj-restuni  35967  pibt2  36287  lindsenlbs  36472  poimirlem29  36506  poimirlem30  36507  poimirlem31  36508  itg2addnclem  36528  itg2addnclem2  36529  ftc1anclem7  36556  ismtyima  36660  lshpkr  37976  psubatN  38615  elpaddn0  38660  pclfinN  38760  diael  39903  dia2dimlem12  39935  dicelval1stN  40048  dicelval2nd  40049  dib2dim  40103  dih2dimbALTN  40105  dihlspsnssN  40192  dvh1dim  40302  lcfrvalsnN  40401  mapdrvallem2  40505  mapdpglem2  40533  hdmap10lem  40699  hdmap11lem2  40702  hdmapoc  40791  sticksstones3  40953  sticksstones17  40968  sticksstones18  40969  isnacs3  41434  aomclem2  41783  kelac1  41791  rngunsnply  41901  safesnsupfiub  42153  intabssd  42256  iunrelexp0  42439  rfovcnvf1od  42741  rfovcnvfvd  42744  fsovrfovd  42746  clsk1indlem3  42780  neik0pk1imk0  42784  ntrneineine0lem  42820  ntrneiel2  42823  ntrneikb  42831  ntrneik4w  42837  mnuop3d  43016  dvconstbi  43079  expgrowth  43080  climsuselem1  44310  climsuse  44311  limcresiooub  44345  iblsplit  44669  iblspltprt  44676  stoweidlem62  44765  stirlinglem11  44787  fourierdlem41  44851  qndenserrnbllem  44997  sge0fodjrnlem  45119  sssmf  45441  smflimsuplem7  45529  fafvelcdm  45865  fafv2elcdm  45929  smonoord  46026  iccpartiltu  46077  iccpartigtl  46078  iccpartiun  46089  iccpartdisj  46092  bgoldbtbndlem2  46461  c0rnghm  46698  issubrng2  46722  rnglidlmmgm  46739  rnglidlmsgrp  46740  rnglidlrng  46741  lidldomn1  46777  rnghmsscmap  46826  rngcsect  46832  funcrngcsetc  46850  rhmsscmap  46872  rhmsscrnghm  46878  ringcsect  46883  funcringcsetc  46887  funcringcsetcALTV2lem9  46896  rhmsubclem4  46941  rhmsubcALTVlem4  46959  lincresunit3lem1  47114  setrec1  47690  setis  47697  vsetrec  47702  pgindnf  47715