Theorem sseld 3966

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

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

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 2793

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 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  sselda  3967  sseldd  3968  ssneld  3969  elelpwi  4551  ssbrd  5109  uniopel  5406  exopxfr2  5715  dmrnssfld  5841  preddowncl  6175  opelf  6539  fvimacnv  6823  ffvelrn  6849  fnsnr  6927  f1imass  7022  onminex  7522  extmptsuppeq  7854  suppssr  7861  dftpos3  7910  wfrlem16  7970  oa00  8185  omordi  8192  omlimcl  8204  omeulem1  8208  nnmordi  8257  mapsnd  8450  ixpf  8484  pw2f1olem  8621  pssnn  8736  findcard3  8761  ixpfi2  8822  fissuni  8829  elfiun  8894  dffi3  8895  ordiso2  8979  ordtypelem7  8988  ixpiunwdom  9055  inf3lem2  9092  cantnfp1lem3  9143  cantnfp1  9144  cantnflem1  9152  cantnf  9156  trcl  9170  r1ordg  9207  rankelb  9253  rankuni2b  9282  rankval4  9296  tcrank  9313  cplem1  9318  carduniima  9522  alephfp  9534  kmlem2  9577  isf32lem3  9777  domtriomlem  9864  axdc3lem2  9873  zorn2lem7  9924  ttukeylem6  9936  iundom2g  9962  fpwwe2lem13  10064  tskss  10180  tskr1om2  10190  inatsk  10200  gruss  10218  gruel  10225  grur1  10242  prlem934  10455  ltexprlem7  10464  supsr  10534  dedekind  10803  supadd  11609  supmullem2  11612  uzind  12075  iccsplit  12872  elfz0add  13007  predfz  13033  fsuppmapnn0fiub  13360  ccatval2  13932  swrdswrd  14067  pfxccatin12lem2a  14089  swrdccatin2  14091  pfxccatpfx2  14099  cshimadifsn0  14192  sqrlem6  14607  isercolllem2  15022  fsumcvg  15069  isumrpcl  15198  fprodcvg  15284  rpnnen2lem4  15570  fproddvdsd  15684  saddisj  15814  sadass  15820  bitsshft  15824  smuval2  15831  smupvallem  15832  smu01lem  15834  smueqlem  15839  reumodprminv  16141  ramub1lem1  16362  firest  16706  mrissmrid  16912  initoeu2lem0  17273  acsfiindd  17787  acsmapd  17788  dirge  17847  issubmnd  17938  issubg2  18294  eqgid  18332  cyccom  18346  dprdff  19134  dprddisj2  19161  ablfac1c  19193  subrgdvds  19549  issubrg2  19555  lssssr  19725  lssats2  19772  lbspss  19854  lsmelval2  19857  lspprat  19925  lbsextlem2  19931  lbsextlem3  19932  lpigen  20029  issubassa3  20097  mplcoe5lem  20248  psgndiflemB  20744  lsmcss  20836  obselocv  20872  f1lindf  20966  mdetdiaglem  21207  cpmadugsumlemF  21484  toprntopon  21533  elcls  21681  clsndisj  21683  elcls3  21691  neindisj  21725  lpval  21747  lpsscls  21749  lpss3  21752  maxlp  21755  restntr  21790  ordtbas2  21799  ordtbas  21800  pnfnei  21828  mnfnei  21829  cncls2  21881  lmcnp  21912  lpcls  21972  hauscmplem  22014  2ndcdisj  22064  kgen2ss  22163  txuni2  22173  ptpjpre1  22179  tx1cn  22217  tx2cn  22218  prdstopn  22236  txlm  22256  imasnopn  22298  imasncld  22299  imasncls  22300  tgqtop  22320  regr1lem  22347  fgss2  22482  uzfbas  22506  ufilmax  22515  uffix2  22532  ufildr  22539  fmfnfmlem1  22562  fmco  22569  flimrest  22591  fclsopn  22622  fclscf  22633  flimfcls  22634  alexsubALTlem4  22658  qustgplem  22729  imasf1oxms  23099  prdsbl  23101  metrest  23134  iccntr  23429  reconnlem2  23435  caucfil  23886  caussi  23900  bcthlem5  23931  ovoliunlem1  24103  shft2rab  24109  sca2rab  24113  ovolicc2  24123  vitalilem2  24210  vitalilem5  24213  mbfinf  24266  i1f1lem  24290  mbfi1fseqlem4  24319  itgss  24412  itgcn  24443  c1liplem1  24593  c1lip1  24594  c1lip3  24596  ply1remlem  24756  plyexmo  24902  lgamucov  25615  fsumvma  25789  logfaclbnd  25798  axlowdimlem16  26743  axcontlem9  26758  edgupgr  26919  upgredg  26922  subgreldmiedg  27065  upgrres1  27095  crctcshwlkn0lem2  27589  wwlksnred  27670  clwwlkccatlem  27767  clwwlkf  27826  wwlksubclwwlk  27837  eupth2lems  28017  sspmval  28510  sspimsval  28515  ubthlem1  28647  shsubcl  28997  shorth  29072  elspansn3  29349  elnlfn  29705  elpjrn  29967  sumdmdlem2  30196  nfpconfp  30377  fimarab  30390  supssd  30445  infssd  30446  xrofsup  30492  cmpcref  31114  cntmeas  31485  1stmbfm  31518  2ndmbfm  31519  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemodife  31755  ballotlemimin  31763  bnj1171  32272  bnj1280  32292  subgrwlk  32379  gonarlem  32641  goalrlem  32643  mrsubrn  32760  elfzm12  32918  trpredtr  33069  trpredmintr  33070  dftrpred3g  33072  trpredrec  33077  sltres  33169  nosepssdm  33190  nodenselem8  33195  nosupno  33203  nosupbday  33205  ontgval  33779  bj-restuni  34391  pibt2  34701  lindsenlbs  34902  poimirlem16  34923  poimirlem29  34936  poimirlem30  34937  poimirlem31  34938  itg2addnclem  34958  itg2addnclem2  34959  ftc1anclem7  34988  ismtyima  35096  lshpkr  36268  psubatN  36906  elpaddn0  36951  pclfinN  37051  diael  38194  dia2dimlem12  38226  dicelval1stN  38339  dicelval2nd  38340  dib2dim  38394  dih2dimbALTN  38396  dihlspsnssN  38483  dvh1dim  38593  lcfrvalsnN  38692  mapdrvallem2  38796  mapdpglem2  38824  hdmap10lem  38990  hdmap11lem2  38993  hdmapoc  39082  isnacs3  39327  aomclem2  39675  kelac1  39683  rngunsnply  39793  intabssd  39905  iunrelexp0  40067  rfovcnvf1od  40370  rfovcnvfvd  40373  fsovrfovd  40375  clsk1indlem3  40413  neik0pk1imk0  40417  ntrneineine0lem  40453  ntrneiel2  40456  ntrneikb  40464  ntrneik4w  40470  mnuop3d  40627  dvconstbi  40686  expgrowth  40687  climsuselem1  41908  climsuse  41909  limcresiooub  41943  iblsplit  42271  iblspltprt  42278  stoweidlem62  42367  stirlinglem11  42389  fourierdlem41  42453  qndenserrnbllem  42599  sge0fodjrnlem  42718  sssmf  43035  smflimsuplem7  43120  fafvelrn  43389  fafv2elrn  43453  smonoord  43551  iccpartiltu  43602  iccpartigtl  43603  iccpartiun  43614  iccpartdisj  43617  bgoldbtbndlem2  43991  c0rnghm  44204  lidldomn1  44212  lidlmmgm  44216  lidlmsgrp  44217  lidlrng  44218  rnghmsscmap  44265  rngcsect  44271  funcrngcsetc  44289  rhmsscmap  44311  rhmsscrnghm  44317  ringcsect  44322  funcringcsetc  44326  funcringcsetcALTV2lem9  44335  rhmsubclem4  44380  rhmsubcALTVlem4  44398  lincresunit3lem1  44554  setrec1  44814  setis  44820  vsetrec  44825