Theorem sseld 3916

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sselda  3917  sseldd  3918  ssneld  3919  elelpwi  4542  ssbrd  5113  uniopel  5424  exopxfr2  5742  dmrnssfld  5868  preddowncl  6224  opelf  6619  fvimacnv  6912  ffvelrn  6941  fnsnr  7019  f1imass  7118  onminex  7629  extmptsuppeq  7975  suppssr  7983  suppssrg  7984  dftpos3  8031  wfrlem16OLD  8126  oa00  8352  omordi  8359  omlimcl  8371  omeulem1  8375  nnmordi  8424  mapsnd  8632  ixpf  8666  pw2f1olem  8816  pssnn  8913  pssnnOLD  8969  findcard3  8987  ixpfi2  9047  fissuni  9054  elfiun  9119  dffi3  9120  ordiso2  9204  ordtypelem7  9213  ixpiunwdom  9279  inf3lem2  9317  cantnfp1lem3  9368  cantnfp1  9369  cantnflem1  9377  cantnf  9381  trpredtr  9408  trpredmintr  9409  dftrpred3g  9412  trpredrec  9415  trcl  9417  r1ordg  9467  rankelb  9513  rankuni2b  9542  rankval4  9556  tcrank  9573  cplem1  9578  carduniima  9783  alephfp  9795  kmlem2  9838  isf32lem3  10042  domtriomlem  10129  axdc3lem2  10138  zorn2lem7  10189  ttukeylem6  10201  iundom2g  10227  fpwwe2lem12  10329  tskss  10445  tskr1om2  10455  inatsk  10465  gruss  10483  gruel  10490  grur1  10507  prlem934  10720  ltexprlem7  10729  supsr  10799  dedekind  11068  supadd  11873  supmullem2  11876  uzind  12342  iccsplit  13146  elfz0add  13284  predfz  13310  fsuppmapnn0fiub  13639  ccatval2  14211  swrdswrd  14346  pfxccatin12lem2a  14368  swrdccatin2  14370  pfxccatpfx2  14378  cshimadifsn0  14471  sqrlem6  14887  isercolllem2  15305  fsumcvg  15352  isumrpcl  15483  fprodcvg  15568  rpnnen2lem4  15854  fproddvdsd  15972  saddisj  16100  sadass  16106  bitsshft  16110  smuval2  16117  smupvallem  16118  smu01lem  16120  smueqlem  16125  reumodprminv  16433  ramub1lem1  16655  firest  17060  mrissmrid  17267  initoeu2lem0  17644  acsfiindd  18186  acsmapd  18187  dirge  18236  issubmnd  18327  issubg2  18685  eqgid  18723  cyccom  18737  dprdff  19530  dprddisj2  19557  ablfac1c  19589  subrgdvds  19953  issubrg2  19959  lssssr  20130  lssats2  20177  lbspss  20259  lsmelval2  20262  lspprat  20330  lbsextlem2  20336  lbsextlem3  20337  lpigen  20440  psgndiflemB  20717  lsmcss  20809  obselocv  20845  f1lindf  20939  issubassa3  20982  mplcoe5lem  21150  mdetdiaglem  21655  cpmadugsumlemF  21933  toprntopon  21982  elcls  22132  clsndisj  22134  elcls3  22142  neindisj  22176  lpval  22198  lpsscls  22200  lpss3  22203  maxlp  22206  restntr  22241  ordtbas2  22250  ordtbas  22251  pnfnei  22279  mnfnei  22280  cncls2  22332  lmcnp  22363  lpcls  22423  hauscmplem  22465  2ndcdisj  22515  kgen2ss  22614  txuni2  22624  ptpjpre1  22630  tx1cn  22668  tx2cn  22669  prdstopn  22687  txlm  22707  imasnopn  22749  imasncld  22750  imasncls  22751  tgqtop  22771  regr1lem  22798  fgss2  22933  uzfbas  22957  ufilmax  22966  uffix2  22983  ufildr  22990  fmfnfmlem1  23013  fmco  23020  flimrest  23042  fclsopn  23073  fclscf  23084  flimfcls  23085  alexsubALTlem4  23109  qustgplem  23180  imasf1oxms  23551  prdsbl  23553  metrest  23586  iccntr  23890  reconnlem2  23896  caucfil  24352  caussi  24366  bcthlem5  24397  ovoliunlem1  24571  shft2rab  24577  sca2rab  24581  ovolicc2  24591  vitalilem2  24678  vitalilem5  24681  mbfinf  24734  i1f1lem  24758  mbfi1fseqlem4  24788  itgss  24881  itgcn  24914  c1liplem1  25065  c1lip1  25066  c1lip3  25068  ply1remlem  25232  plyexmo  25378  lgamucov  26092  fsumvma  26266  logfaclbnd  26275  axlowdimlem16  27228  axcontlem9  27243  edgupgr  27407  upgredg  27410  subgreldmiedg  27553  upgrres1  27583  crctcshwlkn0lem2  28077  wwlksnred  28158  clwwlkccatlem  28254  clwwlkf  28312  wwlksubclwwlk  28323  eupth2lems  28503  sspmval  28996  sspimsval  29001  ubthlem1  29133  shsubcl  29483  shorth  29558  elspansn3  29835  elnlfn  30191  elpjrn  30453  sumdmdlem2  30682  eqrrabd  30750  nfpconfp  30868  fimarab  30881  supssd  30946  infssd  30947  xrofsup  30992  elrspunidl  31508  cmpcref  31702  zarclsiin  31723  cntmeas  32094  1stmbfm  32127  2ndmbfm  32128  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemodife  32364  ballotlemimin  32372  bnj1171  32880  bnj1280  32900  subgrwlk  32994  gonarlem  33256  goalrlem  33258  mrsubrn  33375  elfzm12  33533  xpord2pred  33719  sltres  33792  nosepssdm  33816  nodenselem8  33821  nosupno  33833  nosupbday  33835  noinfbday  33850  elmade  33978  oldssmade  33987  ontgval  34547  bj-restuni  35195  pibt2  35515  lindsenlbs  35699  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  itg2addnclem  35755  itg2addnclem2  35756  ftc1anclem7  35783  ismtyima  35888  lshpkr  37058  psubatN  37696  elpaddn0  37741  pclfinN  37841  diael  38984  dia2dimlem12  39016  dicelval1stN  39129  dicelval2nd  39130  dib2dim  39184  dih2dimbALTN  39186  dihlspsnssN  39273  dvh1dim  39383  lcfrvalsnN  39482  mapdrvallem2  39586  mapdpglem2  39614  hdmap10lem  39780  hdmap11lem2  39783  hdmapoc  39872  sticksstones3  40032  sticksstones17  40047  sticksstones18  40048  isnacs3  40448  aomclem2  40796  kelac1  40804  rngunsnply  40914  intabssd  41024  iunrelexp0  41199  rfovcnvf1od  41501  rfovcnvfvd  41504  fsovrfovd  41506  clsk1indlem3  41542  neik0pk1imk0  41546  ntrneineine0lem  41582  ntrneiel2  41585  ntrneikb  41593  ntrneik4w  41599  mnuop3d  41778  dvconstbi  41841  expgrowth  41842  climsuselem1  43038  climsuse  43039  limcresiooub  43073  iblsplit  43397  iblspltprt  43404  stoweidlem62  43493  stirlinglem11  43515  fourierdlem41  43579  qndenserrnbllem  43725  sge0fodjrnlem  43844  sssmf  44161  smflimsuplem7  44246  fafvelrn  44549  fafv2elrn  44613  smonoord  44711  iccpartiltu  44762  iccpartigtl  44763  iccpartiun  44774  iccpartdisj  44777  bgoldbtbndlem2  45146  c0rnghm  45359  lidldomn1  45367  lidlmmgm  45371  lidlmsgrp  45372  lidlrng  45373  rnghmsscmap  45420  rngcsect  45426  funcrngcsetc  45444  rhmsscmap  45466  rhmsscrnghm  45472  ringcsect  45477  funcringcsetc  45481  funcringcsetcALTV2lem9  45490  rhmsubclem4  45535  rhmsubcALTVlem4  45553  lincresunit3lem1  45708  setrec1  46283  setis  46289  vsetrec  46294