Theorem sseld 3567

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

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  sselda  3568  sseldd  3569  ssneld  3570  elelpwi  4119  ssbrd  4626  uniopel  4903  exopxfr2  5188  dmrnssfld  5305  preddowncl  5624  nfunv  5835  opelf  5978  fvimacnv  6240  ffvelrn  6265  fnsnb  6337  f1imass  6422  onminex  6899  extmptsuppeq  7206  suppssr  7213  dftpos3  7257  wfrlem16  7317  oa00  7526  omordi  7533  omlimcl  7545  omeulem1  7549  nnmordi  7598  mapsn  7785  ixpf  7816  pw2f1olem  7949  pssnn  8063  findcard3  8088  ixpfi2  8147  fissuni  8154  elfiun  8219  dffi3  8220  ordiso2  8303  ordtypelem7  8312  ixpiunwdom  8379  inf3lem2  8409  cantnfp1lem3  8460  cantnfp1  8461  cantnflem1  8469  cantnf  8473  trcl  8487  r1ordg  8524  rankelb  8570  rankuni2b  8599  rankval4  8613  tcrank  8630  cplem1  8635  carduniima  8802  alephfp  8814  kmlem2  8856  isf32lem3  9060  domtriomlem  9147  axdc3lem2  9156  ac6num  9184  zorn2lem7  9207  ttukeylem6  9219  iundom2g  9241  fpwwe2lem13  9343  tskss  9459  tskr1om2  9469  inatsk  9479  gruss  9497  gruel  9504  grur1  9521  prlem934  9734  ltexprlem7  9743  supsr  9812  dedekind  10079  supadd  10868  supmullem2  10871  uzind  11345  iccsplit  12176  elfz0add  12307  predfz  12333  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  ccatval2  13215  swrdswrd  13312  swrdccatin12lem2a  13336  swrdccatin2  13338  swrdccatin12lem2c  13339  swrdccatin12  13342  cshimadifsn0  13427  sqrlem6  13836  isercolllem2  14244  fsumcvg  14290  isumrpcl  14414  fprodcvg  14499  rpnnen2lem4  14785  fproddvdsd  14897  saddisj  15025  sadass  15031  bitsshft  15035  smuval2  15042  smupvallem  15043  smu01lem  15045  smueqlem  15050  reumodprminv  15347  ramub1lem1  15568  firest  15916  mrissmrid  16124  initoeu2lem0  16486  acsfiindd  17000  acsmapd  17001  dirge  17060  issubmnd  17141  issubg2  17432  eqgid  17469  dprdff  18234  dprddisj2  18261  ablfac1c  18293  subrgdvds  18617  issubrg2  18623  lssssr  18774  lssats2  18821  lbspss  18903  lsmelval2  18906  lspprat  18974  lbsextlem2  18980  lbsextlem3  18981  lpigen  19077  mplcoe5lem  19288  psgndiflemB  19765  lsmcss  19855  obselocv  19891  f1lindf  19980  mdetdiaglem  20223  cpmadugsumlemF  20500  elcls  20687  clsndisj  20689  elcls3  20697  neindisj  20731  lpval  20753  lpsscls  20755  lpss3  20758  maxlp  20761  restntr  20796  ordtbas2  20805  ordtbas  20806  pnfnei  20834  mnfnei  20835  cncls2  20887  lmcnp  20918  lpcls  20978  hauscmplem  21019  2ndcdisj  21069  kgen2ss  21168  txuni2  21178  ptpjpre1  21184  tx1cn  21222  tx2cn  21223  prdstopn  21241  txlm  21261  imasnopn  21303  imasncld  21304  imasncls  21305  tgqtop  21325  regr1lem  21352  fgss2  21488  uzfbas  21512  ufilmax  21521  uffix2  21538  ufildr  21545  fmfnfmlem1  21568  fmco  21575  flimrest  21597  fclsopn  21628  fclscf  21639  flimfcls  21640  alexsubALTlem4  21664  qustgplem  21734  imasf1oxms  22104  prdsbl  22106  metrest  22139  iccntr  22432  reconnlem2  22438  caucfil  22889  caussi  22903  bcthlem5  22933  ovoliunlem1  23077  shft2rab  23083  sca2rab  23087  ovolicc2  23097  vitalilem2  23184  vitalilem5  23187  mbfinf  23238  i1f1lem  23262  mbfi1fseqlem4  23291  itgss  23384  itgcn  23415  c1liplem1  23563  c1lip1  23564  c1lip3  23566  ply1remlem  23726  plyexmo  23872  lgamucov  24564  fsumvma  24738  logfaclbnd  24747  axlowdimlem16  25637  axcontlem9  25652  edgupgr  25808  upgredg  25811  wwlknred  26251  wwlknext  26252  clwlkswlks  26286  clwwlkf  26322  wwlksubclwwlk  26332  nbhashuvtx  26443  eupath2  26507  extwwlkfablem2  26605  sspmval  26972  sspimsval  26977  sspph  27094  ubthlem1  27110  shsubcl  27461  shorth  27538  elspansn3  27815  elnlfn  28171  elpjrn  28433  sumdmdlem2  28662  fimarab  28825  supssd  28870  infssd  28871  xrofsup  28923  cmpcref  29245  cntmeas  29616  1stmbfm  29649  2ndmbfm  29650  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemodife  29886  ballotlemimin  29894  bnj142OLD  30048  bnj1171  30322  bnj1280  30342  mrsubrn  30664  elfzm12  30823  trpredtr  30974  trpredmintr  30975  dftrpred3g  30977  trpredrec  30982  sltres  31061  nodenselem8  31087  ontgval  31600  bj-restuni  32231  bj-toprntopon  32244  lindsenlbs  32574  poimirlem16  32595  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  itg2addnclem  32631  itg2addnclem2  32632  ftc1anclem7  32661  ismtyima  32772  lshpkr  33422  psubatN  34059  elpaddn0  34104  pclfinN  34204  diael  35350  dia2dimlem12  35382  dicelval1stN  35495  dicelval2nd  35496  dib2dim  35550  dih2dimbALTN  35552  dihlspsnssN  35639  dvh1dim  35749  lcfrvalsnN  35848  mapdrvallem2  35952  mapdpglem2  35980  hdmap10lem  36149  hdmap11lem2  36152  hdmapoc  36241  isnacs3  36291  aomclem2  36643  kelac1  36651  rngunsnply  36762  intabssd  36935  iunrelexp0  37013  rfovcnvf1od  37318  rfovcnvfvd  37321  fsovrfovd  37323  clsk1indlem3  37361  neik0pk1imk0  37365  ntrneineine0lem  37401  ntrneiel2  37404  ntrneikb  37412  ntrneik4w  37418  dvconstbi  37555  expgrowth  37556  mapsnd  38383  climsuselem1  38674  climsuse  38675  limcresiooub  38709  iblsplit  38858  iblspltprt  38865  stoweidlem62  38955  stirlinglem11  38977  fourierdlem41  39041  qndenserrnbllem  39190  sge0fodjrnlem  39309  sssmf  39625  fafvelrn  39899  smonoord  39944  iccpartiltu  39960  iccpartigtl  39961  iccpartiun  39972  iccpartdisj  39975  bgoldbtbndlem2  40222  pfxccatin12  40288  pfxccatpfx2  40291  subgreldmiedg  40507  upgrres1  40532  nbusgrvtxm1uvtx  40632  crctcsh1wlkn0lem2  41014  wwlksnred  41098  wwlksnext  41099  clwwlksf  41222  wwlksubclwwlks  41232  eupth2lems  41406  c0rnghm  41703  lidldomn1  41711  lidlmmgm  41715  lidlmsgrp  41716  lidlrng  41717  rnghmsscmap  41766  rngcsect  41772  funcrngcsetc  41790  rhmsscmap  41812  rhmsscrnghm  41818  ringcsect  41823  funcringcsetc  41827  funcringcsetcALTV2lem9  41836  rhmsubclem4  41881  rhmsubcALTVlem4  41900  lincresunit3lem1  42062  setrec1  42237  vsetrec  42245