MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sselda Structured version   Unicode version

Theorem sselda 3351
Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014.)
Hypothesis
Ref Expression
sseld.1  |-  ( ph  ->  A  C_  B )
Assertion
Ref Expression
sselda  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )

Proof of Theorem sselda
StepHypRef Expression
1 sseld.1 . . 3  |-  ( ph  ->  A  C_  B )
21sseld 3350 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 429 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  elrel  4937  ffvresb  5869  1stdm  6616  tfrlem1  6827  oeeulem  7032  swoso  7124  erinxp  7166  boxcutc  7298  fundmen  7375  suplub2  7703  supisolem  7712  ordiso2  7721  ordtypelem2  7725  ordtypelem6  7729  ordtypelem7  7730  cantnflt  7872  cantnflem1c  7887  cantnflem1d  7888  cantnflem1  7889  cantnflem3  7891  cantnf  7893  cantnfltOLD  7902  cantnflem1cOLD  7910  cantnflem1dOLD  7911  cantnflem1OLD  7912  cantnflem3OLD  7913  cantnfOLD  7915  cnfcomlem  7924  cnfcom3lem  7928  cnfcomlemOLD  7932  cnfcom3lemOLD  7936  rankelb  8023  rankval3b  8025  ackbij2lem1  8380  ackbij1lem9  8389  ackbij1lem10  8390  ackbij1lem18  8398  ackbij2lem3  8402  ackbij2  8404  fin23lem7  8477  enfin2i  8482  isf32lem9  8522  isf34lem4  8538  fin1a2lem11  8571  hsmexlem4  8590  ttukeylem6  8675  fpwwe2lem8  8796  fpwwe2lem9  8797  fpwwe2  8802  canth4  8806  intwun  8894  wuncval2  8906  inttsk  8933  rankcf  8936  r1tskina  8941  tskuni  8942  elprnq  9152  dedekind  9525  suprub  10283  suprleub  10286  supmul1  10287  supmullem1  10288  supmul  10290  infmrgelb  10302  un0addcl  10605  un0mulcl  10606  suprzcl  10713  zsupss  10936  supxrleub  11281  supxrre  11282  supxrss  11287  infmxrgelb  11289  infmxrre  11290  icoshftf1o  11400  supicc  11425  supiccub  11426  supicclub  11427  supicclub2  11428  uzindi  11795  seqcl  11818  seqfveq  11822  monoord2  11829  sermono  11830  seqsplit  11831  seqcaopr2  11834  seqf1olem2a  11836  seqf1olem2  11838  seqhomo  11845  seqz  11846  seqof2  11856  seqcoll  12208  seqcoll2  12209  ccatval1  12268  ccatass  12278  revccat  12398  rexanre  12826  rexuzre  12832  rexico  12833  limsupgle  12947  limsupval2  12950  limsupgre  12951  limsupbnd2  12953  rlim2lt  12967  rlim3  12968  ello12  12986  lo1bdd2  12994  elo12  12997  rlimclim1  13015  climrlim2  13017  lo1resb  13034  o1resb  13036  rlimcn2  13060  o1of2  13082  rlimsqzlem  13118  isercolllem3  13136  isercoll2  13138  climsup  13139  iseraltlem2  13152  summolem2a  13184  sumss  13193  fsumss  13194  fsumcvg3  13198  fsumsplit  13208  fsum2dlem  13229  fsum0diag2  13242  fsumless  13251  fsumabs  13256  fsumtscopo  13257  fsumparts  13261  fsumrlim  13266  fsumo1  13267  o1fsum  13268  fsumiun  13276  hashuni  13280  hashuniOLD  13281  ackbijnn  13283  binom1dif  13288  incexclem  13291  isumsplit  13295  isumrpcl  13298  isumless  13300  isumltss  13303  supcvg  13310  cvgrat  13335  mertenslem1  13336  rpnnen2  13500  bitsinv2  13631  bitsf1ocnv  13632  bitsinvp1  13637  eulerthlem2  13849  4sqlem11  14008  vdwlem6  14039  ramval  14061  ramcl2lem  14062  restid2  14361  mress  14523  mremre  14534  mreacs  14588  fullsubc  14752  subsubc  14755  funcres  14798  fuciso  14877  setcmon  14947  setcepi  14948  catccatid  14962  drsdirfi  15100  clatglbss  15289  ipodrsfi  15325  isacs3lem  15328  mrelatglb  15346  mrelatlub  15348  issubmnd  15441  ress0g  15442  gsumress  15498  gsumwspan  15515  frmdsssubm  15530  frmdss2  15532  grpinvssd  15594  subginv  15679  issubg2  15687  issubg4  15691  ssnmz  15714  lagsubg2  15733  resghm  15754  conjnmz  15771  conjnmzb  15772  subgga  15809  gass  15810  gasubg  15811  cntzsubm  15844  cntzmhm  15847  f1omvdmvd  15940  f1omvdconj  15943  symggen  15967  psgnunilem5  15991  psgnunilem2  15992  submod  16059  sylow1lem2  16089  sylow1lem3  16090  sylow1lem4  16091  sylow2alem2  16108  sylow2a  16109  sylow2blem2  16111  sylow3lem1  16117  sylow3lem6  16122  lsmssv  16133  lsmub2x  16137  lsmelvalm  16141  lsmcom2  16145  pj1lid  16189  pj1rid  16190  efgrelexlemb  16238  frgpup1  16263  frgpup3lem  16265  cntzcmn  16315  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumzoppg  16430  gsumzoppgOLD  16431  dprdfadd  16498  dprdfaddOLD  16505  dprdres  16513  dprdcntz2  16524  dprddisj2  16525  dprddisj2OLD  16526  dprd2dlem1  16528  dmdprdsplit2lem  16532  ablfac1lem  16557  ablfac1b  16559  ablfac1c  16560  ablfac1eu  16562  pgpfac1lem1  16563  pgpfac1lem2  16564  pgpfac1lem3  16566  pgpfac1lem4  16567  ablfaclem3  16576  rngidss  16659  invrpropd  16778  subrg1  16853  subrginv  16859  subrgunit  16861  cntzsubr  16875  abvres  16902  lssel  16996  islss3  17017  lssintcl  17022  lmhmima  17105  lmhmpreima  17106  lbsel  17136  lbspropd  17157  lsmcv  17199  lspsolvlem  17200  lbsextlem2  17217  lidlsubcl  17275  drngnidl  17288  issubassa2  17392  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  subrgascl  17555  subrgasclcl  17556  zringlpirlem1  17878  zlpirlem1  17883  regsumsupp  18027  ocvocv  18071  ocvlss  18072  pjfo  18115  ocvpj  18117  obsne0  18125  obselocv  18128  dsmmsubg  18143  frlmsslsp  18198  frlmsslspOLD  18199  ofco2  18307  mdetrsca2  18386  mdetunilem9  18401  madugsum  18424  tgclb  18550  tgidm  18560  pptbas  18587  toponmre  18672  neiptoptop  18710  neiptopnei  18711  neiptopreu  18712  clslp  18727  tgrest  18738  perfopn  18764  ordtbas  18771  ordtrest2lem  18782  pnrmcld  18921  ist1-3  18928  isreg2  18956  cncmp  18970  cmpsublem  18977  tgcmp  18979  cmpcld  18980  hauscmplem  18984  2ndcomap  19037  1stcelcls  19040  restlly  19062  lly1stc  19075  kgentopon  19086  llycmpkgen2  19098  txcls  19152  ptclsg  19163  txcnp  19168  txdis1cn  19183  txcmplem1  19189  txkgen  19200  xkoptsub  19202  xkopt  19203  xkococnlem  19207  xkoinjcn  19235  basqtop  19259  tgqtop  19260  kqfvima  19278  kqreglem1  19289  fbelss  19381  fbssfi  19385  fgabs  19427  trfg  19439  uffixfr  19471  uffixsn  19473  elfm2  19496  fmfnfmlem4  19505  fmfnfm  19506  flimnei  19515  flimrest  19531  flimcls  19533  flimsncls  19534  flffbas  19543  fclsrest  19572  fclscmp  19578  alexsublem  19591  ptcmplem3  19601  ptcmplem4  19602  cnextfres  19615  subgntr  19652  opnsubg  19653  clssubg  19654  tgpconcomp  19658  divstgpopn  19665  divstgplem  19666  tsmssubm  19691  tgptsmscls  19699  tgptsmscld  19700  tsmsxplem1  19702  tsmsxplem2  19703  ustssxp  19754  ustuqtop4  19794  utopsnneiplem  19797  utop2nei  19800  isucn2  19829  ucnima  19831  psmetres2  19865  imasdsf1olem  19923  blpnfctr  19986  xmetresbl  19987  mopni2  20043  mopni3  20044  rnblopn  20049  metustexhalfOLD  20113  metustexhalf  20114  metutopOLD  20132  psmetutop  20133  tgioo  20348  xrsmopn  20364  zdis  20368  icccmplem3  20376  reconnlem2  20379  opnreen  20383  metdsf  20399  metdsge  20400  metdsle  20403  metdsre  20404  metnrmlem2  20411  metnrmlem3  20412  fsumcn  20421  climcncf  20451  icccvx  20497  cnheibor  20502  bndth  20505  lebnumlem1  20508  lebnumlem2  20509  pi1grplem  20596  clmneg  20628  nmoleub2lem3  20645  cphsqrcl  20678  cphabscl  20679  clsocv  20737  iscfil2  20752  cfil3i  20755  cfilfcls  20760  cmetcaulem  20774  iscmet3lem2  20778  cfilresi  20781  caussi  20783  lmclim  20788  rrxnm  20870  rrxcph  20871  rrxmval  20879  rrxmetlem  20881  rrxmet  20882  rrxdstprj1  20883  minveclem1  20886  minveclem3b  20890  minveclem4  20894  minveclem6  20896  pjthlem2  20900  ivth2  20914  ivthicc  20917  ovollb2lem  20946  ovoliunlem1  20960  ovolicc2lem4  20978  ioombl1lem4  21017  dyadmax  21053  dyadmbl  21055  opnmbllem  21056  volsup2  21060  volivth  21062  vitalilem5  21067  i1fima  21131  i1fd  21134  itg1val2  21137  itg1cl  21138  itg1ge0  21139  itg11  21144  i1fadd  21148  i1fmul  21149  itg1addlem4  21152  itg1addlem5  21153  i1fmulc  21156  itg1mulc  21157  itg10a  21163  itg1ge0a  21164  itg1climres  21167  mbfi1fseqlem4  21171  mbfi1fseqlem5  21172  mbfi1flim  21176  mbfmullem2  21177  itg2const2  21194  itg2splitlem  21201  itg2split  21202  itg2gt0  21213  itg2cnlem2  21215  iblss  21257  iblss2  21258  itgss3  21267  itgless  21269  itgfsum  21279  itgsplit  21288  itgsplitioo  21290  itggt0  21294  itgcn  21295  ditgcl  21308  ditgswap  21309  ditgsplitlem  21310  ellimc3  21329  perfdvf  21353  dvreslem  21359  dvcnp  21368  dvcnp2  21369  dvaddbr  21387  dvmulbr  21388  dvcjbr  21398  dvmptfsum  21422  dvcnvlem  21423  dvlip  21440  dvlipcn  21441  dvlip2  21442  dv11cn  21448  dvivthlem1  21455  dvivthlem2  21456  dvne0  21458  lhop1lem  21460  lhop2  21462  lhop  21463  dvcvx  21467  dvfsumle  21468  dvfsumge  21469  dvfsumabs  21470  dvfsumlem2  21474  dvfsumlem3  21475  dvfsumrlimge0  21477  dvfsumrlim2  21479  ftc1lem1  21482  ftc1lem4  21486  ftc1lem6  21488  itgsubstlem  21495  ig1peu  21618  plyeq0lem  21653  plypf1  21655  coeeulem  21667  vieta1lem1  21751  vieta1lem2  21752  plyexmo  21754  taylthlem1  21813  taylthlem2  21814  ulmdvlem1  21840  ulmdvlem3  21842  mtest  21844  radcnv0  21856  pserulm  21862  psercnlem2  21864  psercnlem1  21865  psercn  21866  pserdvlem1  21867  pserdvlem2  21868  pserdv  21869  pserdv2  21870  abelthlem3  21873  abelthlem4  21874  abelthlem9  21880  pige3  21954  efif1olem4  21976  efopnlem2  22077  efopn  22078  logccv  22083  loglesqr  22171  rlimcnp  22334  rlimcnp2  22335  xrlimcnp  22337  efrlim  22338  jensenlem1  22355  jensenlem2  22356  jensen  22357  fsumharmonic  22380  wilthlem2  22382  basellem3  22395  basellem5  22397  chtdif  22471  sqff1o  22495  musumsum  22507  muinv  22508  chtublem  22525  fsumvma  22527  vmasum  22530  chpval2  22532  chpchtsum  22533  chpub  22534  perfectlem2  22544  lgsquadlem2  22669  chebbnd1lem1  22693  dchrisumlem2  22714  dchrisumlem3  22715  dchrmusum2  22718  dchrisum0fno1  22735  rpvmasum2  22736  dchrisum0lem1b  22739  dchrisum0lem1  22740  rplogsum  22751  mudivsum  22754  mulogsum  22756  mulog2sumlem2  22759  selberg2lem  22774  chpdifbndlem1  22777  pntrlog2bndlem6  22807  pntrlog2bnd  22808  pntlemj  22827  pntlemf  22829  pntlem3  22833  tglineelsb2  23008  tglinecom  23011  axlowdimlem13  23151  axlowdimlem16  23154  axcontlem4  23164  axcontlem10  23170  umgraex  23208  redwlk  23456  eupares  23547  subgoinv  23746  ubthlem1  24222  ubthlem2  24223  ubthlem3  24224  minvecolem1  24226  minvecolem4  24232  minvecolem5  24233  minvecolem6  24234  shel  24564  chel  24584  ocorth  24645  pjpreeq  24752  chscllem1  24991  chscllem2  24992  spansncvi  25006  off2  25910  xppreima  25915  ofpreima  25935  ofpreima2  25936  fcnvgreu  25942  supxrnemnf  26007  ssnnssfz  26027  iundisjfi  26031  hashunif  26035  toslublem  26079  tosglblem  26081  gsumvsca1  26202  gsumvsca2  26203  ress1r  26208  tpr2rico  26294  ordtrest2NEWlem  26304  ordtconlem1  26306  fsumcvg4  26332  indsum  26431  esummono  26461  gsumesum  26462  elsigass  26520  elsigagen  26542  measiuns  26583  measres  26588  volmeas  26599  sibfof  26678  sitgclg  26680  eulerpartlemsv2  26693  eulerpartlemsf  26694  eulerpartlemsv3  26696  eulerpartlemgc  26697  eulerpartlemv  26699  eulerpartlemb  26703  eulerpartlemf  26705  eulerpartlemr  26709  eulerpartlemgvv  26711  eulerpartlemgu  26712  eulerpartlemgs2  26715  ballotlemsel1i  26847  ballotlemsima  26850  ballotlemfrceq  26863  signsplypnf  26903  signsply0  26904  signstcl  26918  signstf  26919  signstfvn  26922  signstfvp  26924  signsvfn  26935  lgamgulmlem2  26968  lgamgulm2  26974  lgambdd  26975  erdszelem8  27038  cvmscld  27114  cvmsss2  27115  cvmopnlem  27119  cvmlift2lem9  27152  cvmlift2lem11  27154  cvmlift2lem12  27155  cvmliftpht  27159  clim2prod  27354  prodfn0  27360  prodfrec  27361  prodmolem2a  27398  fprodntriv  27406  prodss  27411  fprodss  27412  fprodsplit  27427  fprod2dlem  27442  binomfallfaclem2  27494  trpredelss  27647  sltres  27756  nobndup  27792  nobnddown  27793  nofulllem5  27798  bpolycl  28146  bpolysum  28147  bpolydiflem  28148  supaddc  28370  supadd  28371  opnmbllem0  28380  mblfinlem2  28382  ismblfin  28385  cnambfre  28393  itg2addnclem2  28397  ftc1cnnclem  28418  ftc1cnnc  28419  ftc1anclem6  28425  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  ftc2nc  28429  areacirclem2  28438  areacirclem4  28440  areacirc  28442  opnrebl2  28469  fnessex  28500  fneuni  28501  comppfsc  28532  neibastop1  28533  neibastop2lem  28534  neibastop3  28536  sdclem1  28592  mettrifi  28606  sstotbnd2  28626  equivtotbnd  28630  isbndx  28634  totbndbnd  28641  equivbnd2  28644  cntotbnd  28648  heibor1lem  28661  heiborlem3  28665  heibor  28673  iccbnd  28692  idlcl  28770  divrngidl  28781  ismrcd1  28987  mzpf  29025  mzpindd  29035  fphpdo  29109  pell14qrre  29151  pell14qrne0  29152  elpell14qr2  29156  elpell1qr2  29166  pellfundex  29180  dnnumch3lem  29352  dnnumch3  29353  fnwe2lem2  29357  aomclem4  29363  kelac1  29369  kercvrlsm  29389  hbtlem2  29433  hbtlem5  29437  flcidc  29484  cntzsdrg  29512  itgpowd  29543  areaquad  29545  fmul01  29714  fmulcl  29715  climinf  29732  ibliccsinexp  29744  iblioosinexp  29746  stoweidlem5  29753  stoweidlem11  29759  stoweidlem17  29765  stoweidlem18  29766  stoweidlem26  29774  stoweidlem27  29775  stoweidlem31  29779  stoweidlem35  29783  stoweidlem39  29787  stoweidlem42  29790  stoweidlem43  29791  stoweidlem44  29792  stoweidlem48  29796  stoweidlem51  29799  stoweidlem52  29800  stoweidlem56  29804  stoweidlem57  29805  stoweidlem59  29807  stoweidlem60  29808  stoweidlem61  29809  elfzom1elfzo  30170  zpnn0elfzo  30174  wwlkm1edg  30320  clwlkisclwwlklem2fv1  30397  clwlkisclwwlklem1  30402  clwwlkvbij  30416  clwwisshclwwlem  30423  clwlkfclwwlk  30470  ssnn0ssfz  30693  lincresunit3  30904  bnj1137  31873  bnj1498  31939  lsatfixedN  32494  elpaddn0  33284  diaintclN  34543  dibglbN  34651  dibintclN  34652  dihrnlss  34762  dihglblem3N  34780  dihglblem6  34825  dihintcl  34829  dochkr1  34963  dochkr1OLDN  34964  lcfrlem5  35031  lcfr  35070  mapdrvallem2  35130  hgmapvvlem3  35413  hdmapoc  35419  hlhilocv  35445
  Copyright terms: Public domain W3C validator