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

Theorem sselda 3308
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 3307 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 419 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721    C_ wss 3280
This theorem is referenced by:  elrel  4937  ffvresb  5859  1stdm  6353  oeeulem  6803  swoso  6895  erinxp  6937  boxcutc  7064  fundmen  7139  suplub2  7422  supisolem  7431  ordiso2  7440  ordtypelem2  7444  ordtypelem6  7448  ordtypelem7  7449  cantnflt  7583  cantnflem1c  7599  cantnflem1d  7600  cantnflem1  7601  cantnflem3  7603  cantnf  7605  cnfcomlem  7612  cnfcom3lem  7616  rankelb  7706  rankval3b  7708  ackbij2lem1  8055  ackbij1lem9  8064  ackbij1lem10  8065  ackbij1lem18  8073  ackbij2lem3  8077  ackbij2  8079  fin23lem7  8152  enfin2i  8157  isf32lem9  8197  isf34lem4  8213  fin1a2lem11  8246  hsmexlem4  8265  ttukeylem6  8350  fpwwe2lem8  8468  fpwwe2lem9  8469  fpwwe2  8474  canth4  8478  intwun  8566  wuncval2  8578  inttsk  8605  rankcf  8608  r1tskina  8613  tskuni  8614  elprnq  8824  suprub  9925  suprleub  9928  supmul1  9929  supmullem1  9930  supmul  9932  infmrgelb  9944  un0addcl  10209  un0mulcl  10210  suprzcl  10305  zsupss  10521  supxrleub  10861  supxrre  10862  supxrss  10867  infmxrgelb  10869  infmxrre  10870  icoshftf1o  10976  uzindi  11275  seqcl  11298  seqfveq  11302  monoord2  11309  sermono  11310  seqsplit  11311  seqcaopr2  11314  seqf1olem2a  11316  seqf1olem2  11318  seqhomo  11325  seqz  11326  seqof2  11336  seqcoll  11667  seqcoll2  11668  ccatval1  11700  ccatass  11705  revccat  11753  rexanre  12105  rexuzre  12111  rexico  12112  limsupgle  12226  limsupval2  12229  limsupgre  12230  limsupbnd2  12232  rlim2lt  12246  rlim3  12247  ello12  12265  lo1bdd2  12273  elo12  12276  rlimclim1  12294  climrlim2  12296  lo1resb  12313  o1resb  12315  rlimcn2  12339  o1of2  12361  rlimsqzlem  12397  isercolllem3  12415  isercoll2  12417  climsup  12418  iseraltlem2  12431  summolem2a  12464  sumss  12473  fsumss  12474  fsumcvg3  12478  fsumsplit  12488  fsum2dlem  12509  fsum0diag2  12521  fsumless  12530  fsumabs  12535  fsumtscopo  12536  fsumparts  12540  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  hashuni  12559  hashuniOLD  12560  ackbijnn  12562  binom1dif  12567  incexclem  12571  isumsplit  12575  isumrpcl  12578  isumless  12580  isumltss  12583  supcvg  12590  cvgrat  12615  mertenslem1  12616  rpnnen2  12780  bitsinv2  12910  bitsf1ocnv  12911  bitsinvp1  12916  eulerthlem2  13126  4sqlem11  13278  vdwlem6  13309  ramval  13331  ramcl2lem  13332  restid2  13613  mress  13773  mremre  13784  mreacs  13838  fullsubc  14002  subsubc  14005  funcres  14048  fuciso  14127  setcmon  14197  setcepi  14198  catccatid  14212  drsdirfi  14350  clatglbss  14509  ipodrsfi  14544  isacs3lem  14547  mrelatglb  14565  mrelatlub  14567  issubmnd  14679  gsumress  14732  gsumwspan  14746  frmdsssubm  14761  frmdss2  14763  subginv  14906  issubg2  14914  issubg4  14916  ssnmz  14937  lagsubg2  14956  resghm  14977  conjnmz  14994  conjnmzb  14995  subgga  15032  gass  15033  gasubg  15034  cntzsubm  15089  cntzmhm  15092  submod  15158  sylow1lem2  15188  sylow1lem3  15189  sylow1lem4  15190  sylow2alem2  15207  sylow2a  15208  sylow2blem2  15210  sylow3lem1  15216  sylow3lem6  15221  lsmssv  15232  lsmub2x  15236  lsmelvalm  15240  lsmcom2  15244  pj1lid  15288  pj1rid  15289  efgrelexlemb  15337  frgpup1  15362  frgpup3lem  15364  cntzcmn  15414  gsumval3eu  15468  gsumval3  15469  gsumzaddlem  15481  gsumzoppg  15494  dprdfadd  15533  dprdres  15541  dprdcntz2  15551  dprddisj2  15552  dprd2dlem1  15554  dmdprdsplit2lem  15558  ablfac1lem  15581  ablfac1b  15583  ablfac1c  15584  ablfac1eu  15586  pgpfac1lem1  15587  pgpfac1lem2  15588  pgpfac1lem3  15590  pgpfac1lem4  15591  ablfaclem3  15600  rngidss  15645  invrpropd  15758  subrg1  15833  subrginv  15839  subrgunit  15841  cntzsubr  15855  abvres  15882  lssel  15969  islss3  15990  lssintcl  15995  lmhmima  16078  lmhmpreima  16079  lbsel  16105  lbspropd  16126  lsmcv  16168  lspsolvlem  16169  lbsextlem2  16186  lidlsubcl  16242  drngnidl  16255  issubassa2  16358  mplcoe1  16483  mplcoe2  16485  subrgascl  16513  subrgasclcl  16514  zlpirlem1  16723  ocvocv  16853  ocvlss  16854  pjfo  16897  ocvpj  16899  obsne0  16907  obselocv  16910  tgclb  16990  tgidm  17000  pptbas  17027  toponmre  17112  neiptoptop  17150  neiptopnei  17151  neiptopreu  17152  clslp  17166  tgrest  17177  perfopn  17203  ordtbas  17210  ordtrest2lem  17221  pnrmcld  17360  ist1-3  17367  isreg2  17395  cncmp  17409  cmpsublem  17416  tgcmp  17418  cmpcld  17419  hauscmplem  17423  2ndcomap  17474  1stcelcls  17477  restlly  17499  lly1stc  17512  kgentopon  17523  llycmpkgen2  17535  txcls  17589  ptclsg  17600  txcnp  17605  txdis1cn  17620  txcmplem1  17626  txkgen  17637  xkoptsub  17639  xkopt  17640  xkococnlem  17644  xkoinjcn  17672  basqtop  17696  tgqtop  17697  kqfvima  17715  kqreglem1  17726  fbelss  17818  fbssfi  17822  fgabs  17864  trfg  17876  uffixfr  17908  uffixsn  17910  elfm2  17933  fmfnfmlem4  17942  fmfnfm  17943  flimnei  17952  flimrest  17968  flimcls  17970  flimsncls  17971  flffbas  17980  fclsrest  18009  fclscmp  18015  alexsublem  18028  ptcmplem3  18038  ptcmplem4  18039  cnextfres  18052  subgntr  18089  opnsubg  18090  clssubg  18091  tgpconcomp  18095  divstgpopn  18102  divstgplem  18103  tsmssubm  18125  tgptsmscls  18132  tgptsmscld  18133  tsmsxplem1  18135  tsmsxplem2  18136  ustssxp  18187  ustuqtop4  18227  utopsnneiplem  18230  utop2nei  18233  isucn2  18262  ucnima  18264  psmetres2  18298  imasdsf1olem  18356  blpnfctr  18419  xmetresbl  18420  mopni2  18476  mopni3  18477  rnblopn  18482  metustexhalfOLD  18546  metustexhalf  18547  metutopOLD  18565  psmetutop  18566  tgioo  18780  xrsmopn  18796  zdis  18800  icccmplem3  18808  reconnlem2  18811  opnreen  18815  metdsf  18831  metdsge  18832  metdsle  18835  metdsre  18836  metnrmlem2  18843  metnrmlem3  18844  fsumcn  18853  climcncf  18883  icccvx  18928  cnheibor  18933  bndth  18936  lebnumlem1  18939  lebnumlem2  18940  pi1grplem  19027  clmneg  19059  nmoleub2lem3  19076  cphsqrcl  19100  cphabscl  19101  clsocv  19157  iscfil2  19172  cfil3i  19175  cfilfcls  19180  cmetcaulem  19194  iscmet3lem2  19198  cfilresi  19201  caussi  19203  lmclim  19208  minveclem1  19278  minveclem3b  19282  minveclem4  19286  minveclem6  19288  pjthlem2  19292  ivth2  19305  ivthicc  19308  ovollb2lem  19337  ovoliunlem1  19351  ovolicc2lem4  19369  ioombl1lem4  19408  dyadmax  19443  dyadmbl  19445  opnmbllem  19446  volsup2  19450  volivth  19452  vitalilem5  19457  i1fima  19523  i1fd  19526  itg1val2  19529  itg1cl  19530  itg1ge0  19531  itg11  19536  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  itg1addlem5  19545  i1fmulc  19548  itg1mulc  19549  itg10a  19555  itg1ge0a  19556  itg1climres  19559  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1flim  19568  mbfmullem2  19569  itg2const2  19586  itg2splitlem  19593  itg2split  19594  itg2gt0  19605  itg2cnlem2  19607  iblss  19649  iblss2  19650  itgss3  19659  itgless  19661  itgfsum  19671  itgsplit  19680  itgsplitioo  19682  itggt0  19686  itgcn  19687  ditgcl  19698  ditgswap  19699  ditgsplitlem  19700  ellimc3  19719  perfdvf  19743  dvreslem  19749  dvcnp  19758  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvcjbr  19788  dvmptfsum  19812  dvcnvlem  19813  dvlip  19830  dvlipcn  19831  dvlip2  19832  dv11cn  19838  dvivthlem1  19845  dvivthlem2  19846  dvne0  19848  lhop1lem  19850  lhop2  19852  lhop  19853  dvcvx  19857  dvfsumle  19858  dvfsumge  19859  dvfsumabs  19860  dvfsumlem2  19864  dvfsumlem3  19865  dvfsumrlimge0  19867  dvfsumrlim2  19869  ftc1lem1  19872  ftc1lem4  19876  ftc1lem6  19878  itgsubstlem  19885  ig1peu  20047  plyeq0lem  20082  plypf1  20084  coeeulem  20096  vieta1lem1  20180  vieta1lem2  20181  plyexmo  20183  aaliou3lem2  20213  taylthlem1  20242  taylthlem2  20243  ulmdvlem1  20269  ulmdvlem3  20271  mtest  20273  radcnv0  20285  pserulm  20291  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  pserdv2  20299  abelthlem3  20302  abelthlem4  20303  abelthlem9  20309  pige3  20378  efif1olem4  20400  efopnlem2  20501  efopn  20502  logccv  20507  loglesqr  20595  rlimcnp  20757  rlimcnp2  20758  xrlimcnp  20760  efrlim  20761  jensenlem1  20778  jensenlem2  20779  jensen  20780  fsumharmonic  20803  wilthlem2  20805  basellem3  20818  basellem5  20820  chtdif  20894  sqff1o  20918  musumsum  20930  muinv  20931  chtublem  20948  fsumvma  20950  vmasum  20953  chpval2  20955  chpchtsum  20956  chpub  20957  perfectlem2  20967  lgsquadlem2  21092  chebbnd1lem1  21116  dchrisumlem2  21137  dchrisumlem3  21138  dchrmusum2  21141  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0lem1b  21162  dchrisum0lem1  21163  rplogsum  21174  mudivsum  21177  mulogsum  21179  mulog2sumlem2  21182  selberg2lem  21197  chpdifbndlem1  21200  pntrlog2bndlem6  21230  pntrlog2bnd  21231  pntlemj  21250  pntlemf  21252  pntlem3  21256  umgraex  21311  redwlk  21559  eupares  21650  subgoinv  21849  ubthlem1  22325  ubthlem2  22326  ubthlem3  22327  minvecolem1  22329  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  shel  22666  chel  22686  ocorth  22746  pjpreeq  22853  chscllem1  23092  chscllem2  23093  spansncvi  23107  off2  24007  xppreima  24012  ofpreima  24034  supxrnemnf  24080  ssnnssfz  24101  iundisjfi  24105  hashunif  24111  ress0g  24135  toslub  24144  tosglb  24145  tpr2rico  24263  indsum  24373  esummono  24403  gsumesum  24404  elsigass  24461  elsigagen  24483  measiuns  24524  measres  24529  volmeas  24540  sibfof  24607  sitgclg  24609  ballotlemsel1i  24723  ballotlemsima  24726  ballotlemfrceq  24739  lgamgulmlem2  24767  lgamgulm2  24773  lgambdd  24774  erdszelem8  24837  cvmscld  24913  cvmsss2  24914  cvmopnlem  24918  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift2lem12  24954  cvmliftpht  24958  dedekind  25140  clim2prod  25169  prodfn0  25175  prodfrec  25176  prodmolem2a  25213  fprodntriv  25221  prodss  25226  fprodss  25227  fprodsplit  25242  fprod2dlem  25257  binomfallfaclem2  25307  trpredelss  25449  sltres  25532  nobndup  25568  nobnddown  25569  nofulllem5  25574  axlowdimlem13  25797  axlowdimlem16  25800  axcontlem4  25810  axcontlem10  25816  bpolycl  26002  bpolysum  26003  bpolydiflem  26004  supaddc  26137  supadd  26138  mblfinlem  26143  ismblfin  26146  cnambfre  26154  itg2addnclem2  26156  ftc1cnnclem  26177  ftc1cnnc  26178  areacirclem4  26183  areacirclem5  26185  areacirc  26187  opnrebl2  26214  fnessex  26245  fneuni  26246  comppfsc  26277  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  sdclem1  26337  mettrifi  26353  sstotbnd2  26373  equivtotbnd  26377  isbndx  26381  totbndbnd  26388  equivbnd2  26391  cntotbnd  26395  heibor1lem  26408  heiborlem3  26412  heibor  26420  iccbnd  26439  idlcl  26517  divrngidl  26528  ismrcd1  26642  mzpf  26683  mzpindd  26693  fphpdo  26768  pell14qrre  26810  pell14qrne0  26811  elpell14qr2  26815  elpell1qr2  26825  pellfundex  26839  dnnumch3lem  27011  dnnumch3  27012  fnwe2lem2  27016  aomclem4  27022  kelac1  27029  kercvrlsm  27049  dsmmsubg  27077  frlmsslsp  27116  hbtlem2  27196  hbtlem5  27200  flcidc  27247  f1omvdmvd  27254  f1omvdconj  27257  symggen  27279  psgnunilem5  27285  psgnunilem2  27286  cntzsdrg  27378  fmul01  27577  fmulcl  27578  climinf  27599  ibliccsinexp  27612  iblioosinexp  27614  stoweidlem5  27621  stoweidlem7  27623  stoweidlem11  27627  stoweidlem17  27633  stoweidlem18  27634  stoweidlem26  27642  stoweidlem27  27643  stoweidlem31  27647  stoweidlem35  27651  stoweidlem39  27655  stoweidlem42  27658  stoweidlem43  27659  stoweidlem44  27660  stoweidlem48  27664  stoweidlem51  27667  stoweidlem52  27668  stoweidlem56  27672  stoweidlem57  27673  stoweidlem59  27675  stoweidlem60  27676  stoweidlem61  27677  swrd0swrd  28009  swrdccatin2lem1  28017  swrdccatin2  28018  swrdccatin12  28026  bnj1137  29070  bnj1498  29136  lsatfixedN  29492  elpaddn0  30282  diaintclN  31541  dibglbN  31649  dibintclN  31650  dihrnlss  31760  dihglblem3N  31778  dihglblem6  31823  dihintcl  31827  dochkr1  31961  dochkr1OLDN  31962  lcfrlem5  32029  lcfr  32068  mapdrvallem2  32128  hgmapvvlem3  32411  hdmapoc  32417  hlhilocv  32443
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator