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

Theorem sselda 3489
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 3488 . 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 1804    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  elrel  5095  ffvresb  6047  1stdm  6832  tfrlem1  7047  oeeulem  7252  swoso  7344  erinxp  7387  boxcutc  7514  fundmen  7591  suplub2  7923  supisolem  7934  ordiso2  7943  ordtypelem2  7947  ordtypelem6  7951  ordtypelem7  7952  cantnflt  8094  cantnflem1c  8109  cantnflem1d  8110  cantnflem1  8111  cantnflem3  8113  cantnf  8115  cantnfltOLD  8124  cantnflem1cOLD  8132  cantnflem1dOLD  8133  cantnflem1OLD  8134  cantnflem3OLD  8135  cantnfOLD  8137  cnfcomlem  8146  cnfcom3lem  8150  cnfcomlemOLD  8154  cnfcom3lemOLD  8158  rankelb  8245  rankval3b  8247  ackbij2lem1  8602  ackbij1lem9  8611  ackbij1lem10  8612  ackbij1lem18  8620  ackbij2lem3  8624  ackbij2  8626  fin23lem7  8699  enfin2i  8704  isf32lem9  8744  isf34lem4  8760  fin1a2lem11  8793  hsmexlem4  8812  ttukeylem6  8897  fpwwe2lem8  9018  fpwwe2lem9  9019  fpwwe2  9024  canth4  9028  intwun  9116  wuncval2  9128  inttsk  9155  rankcf  9158  r1tskina  9163  tskuni  9164  elprnq  9372  dedekind  9747  suprub  10511  suprleub  10514  supmul1  10515  supmullem1  10516  supmul  10518  infmrgelb  10530  un0addcl  10836  un0mulcl  10837  suprzcl  10949  zsupss  11182  supxrleub  11529  supxrre  11530  supxrss  11535  infmxrgelb  11537  infmxrre  11538  icoshftf1o  11654  supicc  11679  supiccub  11680  supicclub  11681  supicclub2  11682  elfzom1elfzo  11866  zpnn0elfzo  11870  uzindi  12073  seqcl  12109  seqfveq  12113  monoord2  12120  sermono  12121  seqsplit  12122  seqcaopr2  12125  seqf1olem2a  12127  seqf1olem2  12129  seqhomo  12136  seqz  12137  seqof2  12147  seqcoll  12494  seqcoll2  12495  ccatval1  12577  ccatass  12587  ccatrn  12588  revccat  12722  rexanre  13161  rexuzre  13167  rexico  13168  limsupgle  13282  limsupval2  13285  limsupgre  13286  limsupbnd2  13288  rlim2lt  13302  rlim3  13303  ello12  13321  lo1bdd2  13329  elo12  13332  rlimclim1  13350  climrlim2  13352  lo1resb  13369  o1resb  13371  rlimcn2  13395  o1of2  13417  rlimsqzlem  13453  isercolllem3  13471  isercoll2  13473  climsup  13474  iseraltlem2  13487  summolem2a  13519  sumss  13528  fsumss  13529  fsumcvg3  13533  fsumsplit  13544  fsum2dlem  13567  fsum0diag2  13580  fsumless  13592  fsumabs  13597  telfsumo  13598  fsumparts  13602  fsumrlim  13607  fsumo1  13608  o1fsum  13609  fsumiun  13617  hashuni  13620  ackbijnn  13622  binom1dif  13627  incexclem  13630  isumsplit  13634  isumrpcl  13637  isumless  13639  isumltss  13642  supcvg  13649  cvgrat  13674  mertenslem1  13675  clim2prod  13679  prodfn0  13685  prodfrec  13686  prodmolem2a  13723  fprodntriv  13731  prodss  13736  fprodss  13737  fprodsplit  13752  fprod2dlem  13766  rpnnen2  13941  bitsinv2  14075  bitsf1ocnv  14076  bitsinvp1  14081  eulerthlem2  14294  4sqlem11  14455  vdwlem6  14486  ramval  14508  ramcl2lem  14509  restid2  14810  mress  14972  mremre  14983  mreacs  15037  fullsubc  15198  subsubc  15201  funcres  15244  fuciso  15323  setcmon  15393  setcepi  15394  catccatid  15408  drsdirfi  15546  clatglbss  15736  ipodrsfi  15772  isacs3lem  15775  mrelatglb  15793  mrelatlub  15795  gsumress  15882  issubmnd  15927  ress0g  15928  gsumwspan  15993  frmdsssubm  16008  frmdss2  16010  grpinvssd  16094  subginv  16187  issubg2  16195  issubg4  16199  ssnmz  16222  lagsubg2  16241  resghm  16262  conjnmz  16279  conjnmzb  16280  subgga  16317  gass  16318  gasubg  16319  cntzsubm  16352  cntzmhm  16355  f1omvdmvd  16447  f1omvdconj  16450  symggen  16474  psgnunilem5  16498  psgnunilem2  16499  submod  16568  sylow1lem2  16598  sylow1lem3  16599  sylow1lem4  16600  sylow2alem2  16617  sylow2a  16618  sylow2blem2  16620  sylow3lem1  16626  sylow3lem6  16631  lsmssv  16642  lsmub2x  16646  lsmelvalm  16650  lsmcom2  16654  pj1lid  16698  pj1rid  16699  efgrelexlemb  16747  frgpup1  16772  frgpup3lem  16774  cntzcmn  16827  gsumval3eu  16886  gsumval3OLD  16887  gsumval3  16890  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumzoppg  16946  gsumzoppgOLD  16947  dprdfadd  17039  dprdfaddOLD  17046  dprdres  17054  dprdcntz2  17065  dprddisj2  17066  dprddisj2OLD  17067  dprd2dlem1  17069  dmdprdsplit2lem  17073  ablfac1lem  17098  ablfac1b  17100  ablfac1c  17101  ablfac1eu  17103  pgpfac1lem1  17104  pgpfac1lem2  17105  pgpfac1lem3  17107  pgpfac1lem4  17108  ablfaclem3  17117  ringidss  17204  invrpropd  17326  subrg1  17418  subrginv  17424  subrgunit  17426  cntzsubr  17440  abvres  17467  lssel  17563  islss3  17584  lssintcl  17589  lmhmima  17672  lmhmpreima  17673  lbsel  17703  lbspropd  17724  lsmcv  17766  lspsolvlem  17767  lbsextlem2  17784  lidlsubclOLD  17843  drngnidl  17856  issubassa2  17973  mplcoe1  18106  mplcoe5lem  18109  mplcoe5  18110  mplcoe2OLD  18112  subrgascl  18142  subrgasclcl  18143  zringlpirlem1  18487  zlpirlem1  18492  regsumsupp  18636  ocvocv  18680  ocvlss  18681  pjfo  18724  ocvpj  18726  obsne0  18734  obselocv  18737  dsmmsubg  18752  frlmsslsp  18807  frlmsslspOLD  18808  ofco2  18931  mdetrsca2  19084  mdetunilem9  19100  madugsum  19123  tgclb  19450  tgidm  19460  pptbas  19487  toponmre  19572  neiptoptop  19610  neiptopnei  19611  neiptopreu  19612  clslp  19627  tgrest  19638  perfopn  19664  ordtbas  19671  ordtrest2lem  19682  pnrmcld  19821  ist1-3  19828  isreg2  19856  cncmp  19870  cmpsublem  19877  tgcmp  19879  cmpcld  19880  hauscmplem  19884  2ndcomap  19937  1stcelcls  19940  restlly  19962  lly1stc  19975  comppfsc  20011  kgentopon  20017  llycmpkgen2  20029  txcls  20083  ptclsg  20094  txcnp  20099  txdis1cn  20114  txcmplem1  20120  txkgen  20131  xkoptsub  20133  xkopt  20134  xkococnlem  20138  xkoinjcn  20166  basqtop  20190  tgqtop  20191  kqfvima  20209  kqreglem1  20220  fbelss  20312  fbssfi  20316  fgabs  20358  trfg  20370  uffixfr  20402  uffixsn  20404  elfm2  20427  fmfnfmlem4  20436  fmfnfm  20437  flimnei  20446  flimrest  20462  flimcls  20464  flimsncls  20465  flffbas  20474  fclsrest  20503  fclscmp  20509  alexsublem  20522  ptcmplem3  20532  ptcmplem4  20533  cnextfres  20546  subgntr  20583  opnsubg  20584  clssubg  20585  tgpconcomp  20589  qustgpopn  20596  qustgplem  20597  tsmssubm  20622  tgptsmscls  20630  tgptsmscld  20631  tsmsxplem1  20633  tsmsxplem2  20634  ustssxp  20685  ustuqtop4  20725  utopsnneiplem  20728  utop2nei  20731  isucn2  20760  ucnima  20762  psmetres2  20796  imasdsf1olem  20854  blpnfctr  20917  xmetresbl  20918  mopni2  20974  mopni3  20975  rnblopn  20980  metustexhalfOLD  21044  metustexhalf  21045  metutopOLD  21063  psmetutop  21064  tgioo  21279  xrsmopn  21295  zdis  21299  icccmplem3  21307  reconnlem2  21310  opnreen  21314  metdsf  21330  metdsge  21331  metdsle  21334  metdsre  21335  metnrmlem2  21342  metnrmlem3  21343  fsumcn  21352  climcncf  21382  icccvx  21428  cnheibor  21433  bndth  21436  lebnumlem1  21439  lebnumlem2  21440  pi1grplem  21527  clmneg  21559  nmoleub2lem3  21576  cphsqrtcl  21609  cphabscl  21610  clsocv  21668  iscfil2  21683  cfil3i  21686  cfilfcls  21691  cmetcaulem  21705  iscmet3lem2  21709  cfilresi  21712  caussi  21714  lmclim  21719  rrxnm  21801  rrxcph  21802  rrxmval  21810  rrxmetlem  21812  rrxmet  21813  rrxdstprj1  21814  minveclem1  21817  minveclem3b  21821  minveclem4  21825  minveclem6  21827  pjthlem2  21831  ivth2  21845  ivthicc  21848  ovollb2lem  21877  ovoliunlem1  21891  ovolicc2lem4  21909  ioombl1lem4  21949  dyadmax  21985  dyadmbl  21987  opnmbllem  21988  volsup2  21992  volivth  21994  vitalilem5  21999  i1fima  22063  i1fd  22066  itg1val2  22069  itg1cl  22070  itg1ge0  22071  itg11  22076  i1fadd  22080  i1fmul  22081  itg1addlem4  22084  itg1addlem5  22085  i1fmulc  22088  itg1mulc  22089  itg10a  22095  itg1ge0a  22096  itg1climres  22099  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  mbfi1flim  22108  mbfmullem2  22109  itg2const2  22126  itg2splitlem  22133  itg2split  22134  itg2gt0  22145  itg2cnlem2  22147  iblss  22189  iblss2  22190  itgss3  22199  itgless  22201  itgfsum  22211  itgsplit  22220  itgsplitioo  22222  itggt0  22226  itgcn  22227  ditgcl  22240  ditgswap  22241  ditgsplitlem  22242  ellimc3  22261  perfdvf  22285  dvreslem  22291  dvcnp  22300  dvcnp2  22301  dvaddbr  22319  dvmulbr  22320  dvcjbr  22330  dvmptfsum  22354  dvcnvlem  22355  dvlip  22372  dvlipcn  22373  dvlip2  22374  dv11cn  22380  dvivthlem1  22387  dvivthlem2  22388  dvne0  22390  lhop1lem  22392  lhop2  22394  lhop  22395  dvcvx  22399  dvfsumle  22400  dvfsumge  22401  dvfsumabs  22402  dvfsumlem2  22406  dvfsumlem3  22407  dvfsumrlimge0  22409  dvfsumrlim2  22411  ftc1lem1  22414  ftc1lem4  22418  ftc1lem6  22420  itgsubstlem  22427  ig1peu  22550  plyeq0lem  22585  plypf1  22587  coeeulem  22599  vieta1lem1  22684  vieta1lem2  22685  plyexmo  22687  taylthlem1  22746  taylthlem2  22747  ulmdvlem1  22773  ulmdvlem3  22775  mtest  22777  radcnv0  22789  pserulm  22795  psercnlem2  22797  psercnlem1  22798  psercn  22799  pserdvlem1  22800  pserdvlem2  22801  pserdv  22802  pserdv2  22803  abelthlem3  22806  abelthlem4  22807  abelthlem9  22813  pige3  22888  efif1olem4  22910  efabl  22915  efsubm  22916  efopnlem2  23016  efopn  23017  logccv  23022  loglesqrt  23110  rlimcnp  23273  rlimcnp2  23274  xrlimcnp  23276  efrlim  23277  jensenlem1  23294  jensenlem2  23295  jensen  23296  fsumharmonic  23319  wilthlem2  23321  basellem3  23334  basellem5  23336  chtdif  23410  sqff1o  23434  musumsum  23446  muinv  23447  chtublem  23464  fsumvma  23466  vmasum  23469  chpval2  23471  chpchtsum  23472  chpub  23473  perfectlem2  23483  lgsquadlem2  23608  chebbnd1lem1  23632  dchrisumlem2  23653  dchrisumlem3  23654  dchrmusum2  23657  dchrisum0fno1  23674  rpvmasum2  23675  dchrisum0lem1b  23678  dchrisum0lem1  23679  rplogsum  23690  mudivsum  23693  mulogsum  23695  mulog2sumlem2  23698  selberg2lem  23713  chpdifbndlem1  23716  pntrlog2bndlem6  23746  pntrlog2bnd  23747  pntlemj  23766  pntlemf  23768  pntlem3  23772  tglineelsb2  23990  tglinecom  23993  axlowdimlem13  24235  axlowdimlem16  24238  axcontlem4  24248  axcontlem10  24254  umgraex  24301  edg  24331  redwlk  24586  wwlkm1edg  24713  clwlkisclwwlklem2fv1  24760  clwlkisclwwlklem1  24765  clwwlkvbij  24779  clwwisshclwwlem  24784  clwlkfclwwlk  24822  eupares  24953  subgoinv  25288  ubthlem1  25764  ubthlem2  25765  ubthlem3  25766  minvecolem1  25768  minvecolem4  25774  minvecolem5  25775  minvecolem6  25776  shel  26106  chel  26126  ocorth  26187  pjpreeq  26294  chscllem1  26533  chscllem2  26534  spansncvi  26548  off2  27459  xppreima  27465  ofpreima  27485  ofpreima2  27486  fcnvgreu  27492  supxrnemnf  27561  ssnnssfz  27575  iundisjfi  27579  hashunif  27583  toslublem  27633  tosglblem  27635  gsumvsca1  27751  gsumvsca2  27752  ress1r  27757  reff  27820  locfinreflem  27821  tpr2rico  27872  ordtrest2NEWlem  27882  ordtconlem1  27884  fsumcvg4  27910  indsum  28014  esummono  28044  gsumesum  28045  elsigass  28103  elsigagen  28125  measiuns  28166  measres  28171  volmeas  28181  sibfof  28260  sitgclg  28262  sitgclbn  28263  eulerpartlemsv2  28275  eulerpartlemsf  28276  eulerpartlemsv3  28278  eulerpartlemgc  28279  eulerpartlemv  28281  eulerpartlemb  28285  eulerpartlemf  28287  eulerpartlemr  28291  eulerpartlemgvv  28293  eulerpartlemgu  28294  eulerpartlemgs2  28297  ballotlemsel1i  28429  ballotlemsima  28432  ballotlemfrceq  28445  signsplypnf  28485  signsply0  28486  signstcl  28500  signstf  28501  signstfvn  28504  signstfvp  28506  signsvfn  28517  lgamgulmlem2  28550  lgamgulm2  28556  lgambdd  28557  erdszelem8  28620  cvmscld  28696  cvmsss2  28697  cvmopnlem  28701  cvmlift2lem9  28734  cvmlift2lem11  28736  cvmlift2lem12  28737  cvmliftpht  28741  mclsssvlem  28900  mclsppslem  28921  binomfallfaclem2  29138  trpredelss  29291  sltres  29400  nobndup  29436  nobnddown  29437  nofulllem5  29442  bpolycl  29790  bpolysum  29791  bpolydiflem  29792  supaddc  30017  supadd  30018  opnmbllem0  30026  mblfinlem2  30028  ismblfin  30031  cnambfre  30039  itg2addnclem2  30043  ftc1cnnclem  30064  ftc1cnnc  30065  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  ftc2nc  30075  areacirclem2  30084  areacirclem4  30086  areacirc  30088  opnrebl2  30115  fnessex  30140  fneuni  30141  neibastop1  30153  neibastop2lem  30154  neibastop3  30156  sdclem1  30212  mettrifi  30226  sstotbnd2  30246  equivtotbnd  30250  isbndx  30254  totbndbnd  30261  equivbnd2  30264  cntotbnd  30268  heibor1lem  30281  heiborlem3  30285  heibor  30293  iccbnd  30312  idlcl  30390  divrngidl  30401  ismrcd1  30606  mzpf  30644  mzpindd  30654  fphpdo  30727  pell14qrre  30769  pell14qrne0  30770  elpell14qr2  30774  elpell1qr2  30784  pellfundex  30798  dnnumch3lem  30968  dnnumch3  30969  fnwe2lem2  30973  aomclem4  30979  kelac1  30985  kercvrlsm  31005  hbtlem2  31049  hbtlem5  31053  flcidc  31099  cntzsdrg  31127  itgpowd  31158  areaquad  31160  radcnvrat  31171  infmxrss  31446  ssfiunibd  31463  iccshift  31512  iocopn  31514  eliccelioc  31515  iooshift  31516  icoiccdif  31518  icoopn  31519  fmul01  31528  fmulcl  31529  fprodexp  31554  fprodabs2  31556  climinf  31566  mullimc  31576  mullimcf  31583  idlimc  31586  limcperiod  31588  limcrecl  31589  limcresiooub  31602  limcresioolb  31603  limcleqr  31604  addlimc  31608  limclner  31611  cncfmptssg  31626  cncfshift  31630  cncfperiod  31635  cncfuni  31643  icccncfext  31644  dvmptidg  31666  dvbdfbdioolem1  31679  ioodvbdlimc1lem1  31682  dvmptfprodlem  31695  dvnprodlem1  31697  dvnprodlem2  31698  ibliccsinexp  31703  iblioosinexp  31705  itgcoscmulx  31722  itgsincmulx  31727  itgioocnicc  31730  itgiccshift  31733  itgperiod  31734  itgsbtaddcnst  31735  stoweidlem5  31741  stoweidlem11  31747  stoweidlem17  31753  stoweidlem18  31754  stoweidlem26  31762  stoweidlem27  31763  stoweidlem31  31767  stoweidlem35  31771  stoweidlem39  31775  stoweidlem42  31778  stoweidlem43  31779  stoweidlem44  31780  stoweidlem48  31784  stoweidlem51  31787  stoweidlem52  31788  stoweidlem56  31792  stoweidlem57  31793  stoweidlem59  31795  stoweidlem60  31796  stoweidlem61  31797  dirkeritg  31838  dirkercncflem2  31840  dirkercncflem4  31842  fourierdlem38  31881  fourierdlem39  31882  fourierdlem42  31885  fourierdlem46  31889  fourierdlem48  31891  fourierdlem49  31892  fourierdlem51  31894  fourierdlem53  31896  fourierdlem56  31899  fourierdlem57  31900  fourierdlem58  31901  fourierdlem64  31907  fourierdlem66  31909  fourierdlem68  31911  fourierdlem69  31912  fourierdlem70  31913  fourierdlem71  31914  fourierdlem72  31915  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem76  31919  fourierdlem79  31922  fourierdlem80  31923  fourierdlem81  31924  fourierdlem83  31926  fourierdlem87  31930  fourierdlem90  31933  fourierdlem93  31936  fourierdlem95  31938  fourierdlem97  31940  fourierdlem101  31944  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem112  31955  fourierdlem113  31956  fouriersw  31968  etransclem1  31972  etransclem4  31975  etransclem17  31988  etransclem18  31989  etransclem20  31991  etransclem46  32017  elpwdifsn  32250  rhmsubclem3  32764  rhmsubclem4  32765  rhmsubcOLDlem4  32784  ssnn0ssfz  32806  lincresunit3  32952  bnj1137  33919  bnj1498  33985  lsatfixedN  34609  elpaddn0  35399  diaintclN  36660  dibglbN  36768  dibintclN  36769  dihrnlss  36879  dihglblem3N  36897  dihglblem6  36942  dihintcl  36946  dochkr1  37080  dochkr1OLDN  37081  lcfrlem5  37148  lcfr  37187  mapdrvallem2  37247  hgmapvvlem3  37530  hdmapoc  37536  hlhilocv  37562
  Copyright terms: Public domain W3C validator