Theorem sseld 3930

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-clel 2835  df-ss 3916

This theorem is used by:  sselda  3931  sseldd  3932  ssneld  3933  eqrrabd  4034  elelpwi  4567  ssbrd  5148  uniopel  5493  exopxfr2  5824  dmrnssfld  5958  preddowncl  6330  opelf  6736  elfvunirn  6908  fimarab  6952  fvimacnv  7045  ffvelcdm  7074  fnsnr  7161  f1imass  7261  onminex  7801  xpord2pred  8143  extmptsuppeq  8186  suppssr  8193  suppssrg  8194  dftpos3  8242  oa00  8546  omordi  8553  omlimcl  8565  omeulem1  8569  nnmordi  8619  mapsnd  8893  ixpf  8927  pw2f1olem  9079  pssnn  9163  findcard3  9253  ixpfi2  9317  fissuni  9324  elfiun  9400  dffi3  9401  supssd  9433  infssd  9464  ordiso2  9487  ordtypelem7  9496  ixpiunwdom  9562  inf3lem2  9608  cantnfp1lem3  9659  cantnfp1  9660  cantnflem1  9668  cantnf  9672  trcl  9707  r1ordg  9760  rankelb  9806  rankuni2b  9835  rankval4  9849  tcrank  9866  cplem1  9889  cplem1OLD  9890  carduniima  10099  alephfp  10111  kmlem2  10154  isf32lem3  10357  domtriomlem  10444  axdc3lem2  10453  zorn2lem7  10504  ttukeylem6  10516  iundom2g  10548  fpwwe2lem12  10651  tskss  10767  tskr1om2  10777  inatsk  10787  gruss  10805  gruel  10812  grur1  10829  prlem934  11042  ltexprlem7  11051  supsr  11121  dedekind  11397  supadd  12207  supmullem2  12210  uzind  12713  iccsplit  13538  elfz0add  13681  predfz  13708  elfzoextl  13777  fsuppmapnn0fiub  14055  ccatval2  14643  swrdswrd  14774  pfxccatin12lem2a  14796  swrdccatin2  14798  pfxccatpfx2  14806  cshimadifsn0  14901  01sqrexlem6  15334  isercolllem2  15753  fsumcvg  15798  isumrpcl  15932  fprodcvg  16017  rpnnen2lem4  16305  fproddvdsd  16425  saddisj  16555  sadass  16561  bitsshft  16565  smuval2  16572  smupvallem  16573  smu01lem  16575  smueqlem  16580  reumodprminv  16896  ramub1lem1  17118  firest  17517  mrissmrid  17729  initoeu2lem0  18102  acsfiindd  18641  acsmapd  18642  dirge  18691  chndss  18704  issubmnd  18866  issubg2  19265  eqgid  19305  cyccom  19331  dprdff  20141  dprddisj2  20168  ablfac1c  20200  c0rnghm  20697  issubrng2  20720  subrgdvds  20748  issubrg2  20754  rnghmsscmap  20792  rngcsect  20798  funcrngcsetc  20802  rhmsscmap  20821  rhmsscrnghm  20827  ringcsect  20832  funcringcsetc  20836  rhmsubclem4  20850  lssssr  21138  lssats2  21184  lbspss  21266  lsmelval2  21269  lspprat  21340  lbsextlem2  21346  lbsextlem3  21347  rnglidlmmgm  21442  rnglidlmsgrp  21443  rnglidlrng  21444  df2idl2crng  21484  lpigen  21566  psgndiflemB  21813  lsmcss  21905  obselocv  21941  f1lindf  22035  lindsenlbs  22064  issubassa3  22081  mplcoe5lem  22255  mdetdiaglem  22820  cpmadugsumlemF  23101  toprntopon  23150  elcls  23298  clsndisj  23300  elcls3  23308  neindisj  23342  lpval  23364  lpsscls  23366  lpss3  23369  maxlp  23372  restntr  23407  ordtbas2  23416  ordtbas  23417  pnfnei  23445  mnfnei  23446  cncls2  23498  lmcnp  23529  lpcls  23589  hauscmplem  23631  2ndcdisj  23682  kgen2ss  23781  txuni2  23791  ptpjpre1  23797  tx1cn  23835  tx2cn  23836  prdstopn  23854  txlm  23874  imasnopn  23916  imasncld  23917  imasncls  23918  tgqtop  23938  regr1lem  23965  fgss2  24100  uzfbas  24124  ufilmax  24133  uffix2  24150  ufildr  24157  fmfnfmlem1  24180  fmco  24187  flimrest  24209  fclsopn  24240  fclscf  24251  flimfcls  24252  alexsubALTlem4  24276  qustgplem  24347  imasf1oxms  24715  prdsbl  24717  metrest  24750  iccntr  25048  reconnlem2  25054  caucfil  25511  caussi  25525  bcthlem5  25556  ovoliunlem1  25730  shft2rab  25736  sca2rab  25740  ovolicc2  25750  vitalilem2  25837  vitalilem5  25840  mbfinf  25893  i1f1lem  25917  mbfi1fseqlem4  25946  itgss  26039  itgcn  26072  c1liplem1  26223  c1lip1  26224  c1lip3  26226  ply1remlem  26390  plyconz  26540  plyexmo  26545  taylply2  26604  lgamucov  27274  fsumvma  27449  logfaclbnd  27458  ltsres  27898  nosepssdm  27922  nodenselem8  27927  nosupno  27939  nosupbday  27941  noinfbday  27956  elmade  28122  oldssmade  28132  mulsproplem13  28393  mulsproplem14  28394  precsexlem10  28481  bdayons  28541  uzsind  28670  axlowdimlem16  29414  axcontlem9  29429  edgupgr  29591  upgredg  29594  subgreldmiedg  29743  upgrres1  29773  subgrwlk  30148  crctcshwlkn0lem2  30279  wwlksnred  30360  clwwlkccatlem  30459  clwwlkf  30517  wwlksubclwwlk  30528  eupth2lems  30718  sspmval  31214  sspimsval  31219  ubthlem1  31351  shsubcl  31701  shorth  31776  elspansn3  32053  elnlfn  32409  elpjrn  32671  sumdmdlem2  32900  nfpconfp  33105  xrofsup  33238  elrspunidl  33856  ressply1mon1p  33978  fldextrspunlsplem  34183  cmpcref  34360  zarclsiin  34381  cntmeas  34737  1stmbfm  34771  2ndmbfm  34772  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemodife  35009  ballotlemimin  35017  bnj1171  35509  bnj1280  35529  r1filimi  35611  gonarlem  35973  goalrlem  35975  mrsubrn  36092  elfzm12  36254  ontgval  37050  elttctr  37124  bj-restuni  37847  pibt2  38171  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  itg2addnclem  38420  itg2addnclem2  38421  ftc1anclem7  38448  ismtyima  38553  suceldisj  39566  lshpkr  39990  psubatN  40628  elpaddn0  40673  pclfinN  40773  diael  41916  dia2dimlem12  41948  dicelval1stN  42061  dicelval2nd  42062  dib2dim  42116  dih2dimbALTN  42118  dihlspsnssN  42205  dvh1dim  42315  lcfrvalsnN  42414  mapdrvallem2  42518  mapdpglem2  42546  hdmap10lem  42712  hdmap11lem2  42715  hdmapoc  42804  primrootscoprbij  42968  primrootspoweq0  42972  aks6d1c2  42996  sticksstones3  43014  sticksstones17  43029  sticksstones18  43030  unitscyglem2  43062  unitscyglem4  43064  unitscyglem5  43065  isnacs3  43555  aomclem2  43896  kelac1  43904  rngunsnply  44010  safesnsupfiub  44256  intabssd  44359  iunrelexp0  44542  rfovcnvf1od  44844  rfovcnvfvd  44847  fsovrfovd  44849  clsk1indlem3  44883  neik0pk1imk0  44887  ntrneineine0lem  44923  ntrneiel2  44926  ntrneikb  44934  ntrneik4w  44940  mnuop3d  45095  dvconstbi  45158  expgrowth  45159  modelaxreplem2  45802  modelaxreplem3  45803  climsuselem1  46437  climsuse  46438  limcresiooub  46470  iblsplit  46794  iblspltprt  46801  stoweidlem62  46890  stirlinglem11  46912  fourierdlem41  46976  qndenserrnbllem  47122  sge0fodjrnlem  47244  smflimsuplem7  47654  fafvelcdm  48058  fafv2elcdm  48122  ceilhalfelfzo1  48222  smonoord  48265  muldvdsfacm1  48275  iccpartiltu  48322  iccpartigtl  48323  iccpartiun  48334  iccpartdisj  48337  bgoldbtbndlem2  48722  gpgedgvtx1  48978  lidldomn1  49146  rhmsubcALTVlem4  49199  funcringcsetcALTV2lem9  49213  lincresunit3lem1  49409  setrec1  50617  setis  50624  vsetrec  50629  pgindnf  50642