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

Theorem sselda 3470
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 3469 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 430 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1870    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  elrel  4957  ffvresb  6069  1stdm  6854  tfrlem1  7102  oeeulem  7310  swoso  7402  erinxp  7445  boxcutc  7573  fundmen  7650  suplub2  7981  supisolem  7995  ordiso2  8030  ordtypelem2  8034  ordtypelem6  8038  ordtypelem7  8039  cantnflt  8176  cantnflem1c  8191  cantnflem1d  8192  cantnflem1  8193  cantnflem3  8195  cantnf  8197  cnfcomlem  8203  cnfcom3lem  8207  rankelb  8294  rankval3b  8296  ackbij2lem1  8647  ackbij1lem9  8656  ackbij1lem10  8657  ackbij1lem18  8665  ackbij2lem3  8669  ackbij2  8671  fin23lem7  8744  enfin2i  8749  isf32lem9  8789  isf34lem4  8805  fin1a2lem11  8838  hsmexlem4  8857  ttukeylem6  8942  fpwwe2lem8  9061  fpwwe2lem9  9062  fpwwe2  9067  canth4  9071  intwun  9159  wuncval2  9171  inttsk  9198  rankcf  9201  r1tskina  9206  tskuni  9207  elprnq  9415  dedekind  9796  suprub  10570  suprleub  10573  supaddc  10574  supadd  10575  supmul1  10576  supmullem1  10577  supmul  10579  infmrgelbOLD  10595  un0addcl  10903  un0mulcl  10904  suprzcl  11015  zsupss  11253  supxrleub  11612  supxrre  11613  supxrss  11618  infxrgelb  11621  infxrre  11622  infmxrgelbOLD  11625  infmxrreOLD  11626  infxrss  11628  infmxrssOLD  11629  icoshftf1o  11753  supicc  11778  supiccub  11779  supicclub  11780  supicclub2  11781  elfzoext  11968  elfzom1elfzo  11979  zpnn0elfzo  11983  uzindi  12191  seqcl  12230  seqfveq  12234  monoord2  12241  sermono  12242  seqsplit  12243  seqcaopr2  12246  seqf1olem2a  12248  seqf1olem2  12250  seqhomo  12257  seqz  12258  seqof2  12268  seqcoll  12621  seqcoll2  12622  ccatass  12719  ccatrn  12720  revccat  12856  rexanre  13388  rexuzre  13394  rexico  13395  limsupgle  13513  limsupval2  13518  limsupval2OLD  13519  limsupgre  13520  limsupgreOLD  13521  limsupbnd2  13524  limsupbnd2OLD  13525  rlim2lt  13539  rlim3  13540  ello12  13558  lo1bdd2  13566  elo12  13569  rlimclim1  13587  climrlim2  13589  lo1resb  13606  o1resb  13608  rlimcn2  13632  o1of2  13654  rlimsqzlem  13690  isercolllem3  13708  isercoll2  13710  climsup  13711  iseraltlem2  13727  summolem2a  13759  sumss  13768  fsumss  13769  fsumcvg3  13773  fsumsplit  13784  fsum2dlem  13809  fsum0diag2  13822  fsumless  13834  fsumabs  13839  telfsumo  13840  fsumparts  13844  fsumrlim  13849  fsumo1  13850  o1fsum  13851  fsumiun  13859  hashuni  13862  ackbijnn  13864  binom1dif  13869  incexclem  13872  isumsplit  13876  isumrpcl  13879  isumless  13881  isumltss  13884  supcvg  13892  cvgrat  13917  mertenslem1  13918  clim2prod  13922  prodfn0  13928  prodfrec  13929  prodmolem2a  13966  fprodntriv  13974  prodss  13979  fprodss  13980  fprodsplit  13998  fprod2dlem  14012  binomfallfaclem2  14071  bpolycl  14083  bpolysum  14084  bpolydiflem  14085  rpnnen2  14256  bitsinv2  14391  bitsf1ocnv  14392  bitsinvp1  14397  absproddvds  14552  absprodnn  14553  coprmprod  14640  coprmproddvdslem  14641  eulerthlem2  14690  4sqlem11  14853  vdwlem6  14890  ramval  14914  ramvalOLD  14915  ramcl2lem  14916  ramcl2lemOLD  14917  prmgaplcmlem1  14963  prmgaplcmlem1OLD  14966  restid2  15279  mress  15441  mremre  15452  mreacs  15506  fullsubc  15697  subsubc  15700  funcres  15743  fuciso  15822  initoeu2lem1  15851  initoeu2  15853  setcmon  15924  setcepi  15925  catccatid  15939  drsdirfi  16125  clatglbss  16315  ipodrsfi  16351  isacs3lem  16354  mrelatglb  16372  mrelatlub  16374  gsumress  16461  issubmnd  16506  ress0g  16507  gsumwspan  16572  frmdsssubm  16587  frmdss2  16589  grpinvssd  16673  subginv  16766  issubg2  16774  issubg4  16778  ssnmz  16801  lagsubg2  16820  resghm  16841  conjnmz  16858  conjnmzb  16859  subgga  16896  gass  16897  gasubg  16898  cntzsubm  16931  cntzmhm  16934  f1omvdmvd  17026  f1omvdconj  17029  symggen  17053  psgnunilem5  17077  psgnunilem2  17078  submod  17147  sylow1lem2  17177  sylow1lem3  17178  sylow1lem4  17179  sylow2alem2  17196  sylow2a  17197  sylow2blem2  17199  sylow3lem1  17205  sylow3lem6  17210  lsmssv  17221  lsmub2x  17225  lsmelvalm  17229  lsmcom2  17233  pj1lid  17277  pj1rid  17278  efgrelexlemb  17326  frgpup1  17351  frgpup3lem  17353  cntzcmn  17406  gsumval3eu  17464  gsumval3  17467  gsumzaddlem  17480  gsumzoppg  17503  dprdfadd  17579  dprdres  17587  dprdcntz2  17597  dprddisj2  17598  dprd2dlem1  17600  dmdprdsplit2lem  17604  ablfac1lem  17627  ablfac1b  17629  ablfac1c  17630  ablfac1eu  17632  pgpfac1lem1  17633  pgpfac1lem2  17634  pgpfac1lem3  17636  pgpfac1lem4  17637  ablfaclem3  17646  ringidss  17733  invrpropd  17852  subrg1  17944  subrginv  17950  subrgunit  17952  cntzsubr  17966  abvres  17993  lssel  18087  islss3  18108  lssintcl  18113  lmhmima  18196  lmhmpreima  18197  lbsel  18227  lbspropd  18248  lsmcv  18290  lspsolvlem  18291  lbsextlem2  18308  lidlsubclOLD  18366  drngnidl  18379  issubassa2  18495  mplcoe1  18615  mplcoe5lem  18617  mplcoe5  18618  subrgascl  18647  subrgasclcl  18648  zringlpirlem1  18978  regsumsupp  19112  ocvocv  19156  ocvlss  19157  pjfo  19200  ocvpj  19202  obsne0  19210  obselocv  19213  dsmmsubg  19228  frlmsslsp  19276  ofco2  19398  mdetrsca2  19551  mdetunilem9  19567  madugsum  19590  tgclb  19908  tgidm  19918  pptbas  19945  toponmre  20031  neiptoptop  20069  neiptopnei  20070  neiptopreu  20071  clslp  20086  tgrest  20097  perfopn  20123  ordtbas  20130  ordtrest2lem  20141  pnrmcld  20280  ist1-3  20287  isreg2  20315  cncmp  20329  cmpsublem  20336  tgcmp  20338  cmpcld  20339  hauscmplem  20343  2ndcomap  20395  1stcelcls  20398  restlly  20420  lly1stc  20433  comppfsc  20469  kgentopon  20475  llycmpkgen2  20487  txcls  20541  ptclsg  20552  txcnp  20557  txdis1cn  20572  txcmplem1  20578  txkgen  20589  xkoptsub  20591  xkopt  20592  xkococnlem  20596  xkoinjcn  20624  basqtop  20648  tgqtop  20649  kqfvima  20667  kqreglem1  20678  fbelss  20770  fbssfi  20774  fgabs  20816  trfg  20828  uffixfr  20860  uffixsn  20862  elfm2  20885  fmfnfmlem4  20894  fmfnfm  20895  flimnei  20904  flimrest  20920  flimcls  20922  flimsncls  20923  flffbas  20932  fclsrest  20961  fclscmp  20967  alexsublem  20981  ptcmplem3  20991  ptcmplem4  20992  cnextfres1  21005  subgntr  21043  opnsubg  21044  clssubg  21045  tgpconcomp  21049  qustgpopn  21056  qustgplem  21057  tsmssubm  21079  tgptsmscls  21086  tgptsmscld  21087  tsmsxplem1  21089  tsmsxplem2  21090  ustssxp  21141  ustuqtop4  21181  utopsnneiplem  21184  utop2nei  21187  isucn2  21216  ucnima  21218  psmetres2  21252  imasdsf1olem  21310  blpnfctr  21373  xmetresbl  21374  mopni2  21430  mopni3  21431  rnblopn  21436  metustexhalf  21493  psmetutop  21504  tgioo  21716  xrsmopn  21732  zdis  21736  icccmplem3  21744  reconnlem2  21747  opnreen  21751  metdsf  21767  metdsge  21768  metdsle  21771  metdsre  21772  metnrmlem2  21779  metnrmlem3  21780  fsumcn  21789  climcncf  21819  icccvx  21865  cnheibor  21870  bndth  21873  lebnumlem1  21876  lebnumlem2  21877  pi1grplem  21964  clmneg  21996  nmoleub2lem3  22013  cphsqrtcl  22046  cphabscl  22047  clsocv  22105  iscfil2  22120  cfil3i  22123  cfilfcls  22128  cmetcaulem  22142  iscmet3lem2  22146  cfilresi  22149  caussi  22151  lmclim  22156  rrxnm  22234  rrxcph  22235  rrxmval  22243  rrxmetlem  22245  rrxmet  22246  rrxdstprj1  22247  minveclem1  22250  minveclem3b  22254  minveclem4  22258  minveclem6  22260  pjthlem2  22264  ivth2  22278  ivthicc  22281  ovollb2lem  22310  ovoliunlem1  22324  ovolicc2lem4  22342  ioombl1lem4  22382  dyadmax  22424  dyadmbl  22426  opnmbllem  22427  volsup2  22431  volivth  22433  vitalilem5  22438  i1fima  22504  i1fd  22507  itg1val2  22510  itg1cl  22511  itg1ge0  22512  itg11  22517  i1fadd  22521  i1fmul  22522  itg1addlem4  22525  itg1addlem5  22526  i1fmulc  22529  itg1mulc  22530  itg10a  22536  itg1ge0a  22537  itg1climres  22540  mbfi1fseqlem4  22544  mbfi1fseqlem5  22545  mbfi1flim  22549  mbfmullem2  22550  itg2const2  22567  itg2splitlem  22574  itg2split  22575  itg2gt0  22586  itg2cnlem2  22588  iblss  22630  iblss2  22631  itgss3  22640  itgless  22642  itgfsum  22652  itgsplit  22661  itgsplitioo  22663  itggt0  22667  itgcn  22668  ditgcl  22681  ditgswap  22682  ditgsplitlem  22683  ellimc3  22702  perfdvf  22726  dvreslem  22732  dvcnp  22741  dvcnp2  22742  dvaddbr  22760  dvmulbr  22761  dvcjbr  22771  dvmptfsum  22795  dvcnvlem  22796  dvlip  22813  dvlipcn  22814  dvlip2  22815  dv11cn  22821  dvivthlem1  22828  dvivthlem2  22829  dvne0  22831  lhop1lem  22833  lhop2  22835  lhop  22836  dvcvx  22840  dvfsumle  22841  dvfsumge  22842  dvfsumabs  22843  dvfsumlem2  22847  dvfsumlem3  22848  dvfsumrlimge0  22850  dvfsumrlim2  22852  ftc1lem1  22855  ftc1lem4  22859  ftc1lem6  22861  itgsubstlem  22868  ig1peu  22988  plyeq0lem  23023  plypf1  23025  coeeulem  23037  vieta1lem1  23122  vieta1lem2  23123  plyexmo  23125  taylthlem1  23184  taylthlem2  23185  ulmdvlem1  23211  ulmdvlem3  23213  mtest  23215  radcnv0  23227  pserulm  23233  psercnlem2  23235  psercnlem1  23236  psercn  23237  pserdvlem1  23238  pserdvlem2  23239  pserdv  23240  pserdv2  23241  abelthlem3  23244  abelthlem4  23245  abelthlem9  23251  pige3  23328  efif1olem4  23350  efabl  23355  efsubm  23356  efopnlem2  23458  efopn  23459  logccv  23464  loglesqrt  23554  rlimcnp  23747  rlimcnp2  23748  xrlimcnp  23750  efrlim  23751  jensenlem1  23768  jensenlem2  23769  jensen  23770  fsumharmonic  23793  lgamgulmlem2  23811  lgamgulm2  23817  lgambdd  23818  wilthlem2  23850  basellem3  23863  basellem5  23865  chtdif  23939  sqff1o  23963  musumsum  23975  muinv  23976  chtublem  23993  fsumvma  23995  vmasum  23998  chpval2  24000  chpchtsum  24001  chpub  24002  perfectlem2  24012  lgsquadlem2  24137  chebbnd1lem1  24161  dchrisumlem2  24182  dchrisumlem3  24183  dchrmusum2  24186  dchrisum0fno1  24203  rpvmasum2  24204  dchrisum0lem1b  24207  dchrisum0lem1  24208  rplogsum  24219  mudivsum  24222  mulogsum  24224  mulog2sumlem2  24227  selberg2lem  24242  chpdifbndlem1  24245  pntrlog2bndlem6  24275  pntrlog2bnd  24276  pntlemj  24295  pntlemf  24297  pntlem3  24301  tglineelsb2  24527  tglinecom  24530  axlowdimlem13  24821  axlowdimlem16  24824  axcontlem4  24834  axcontlem10  24840  umgraex  24887  edg  24917  redwlk  25172  wwlkm1edg  25299  clwlkisclwwlklem2fv1  25346  clwlkisclwwlklem1  25351  clwwlkvbij  25365  clwwisshclwwlem  25370  clwlkfclwwlk  25408  eupares  25539  subgoinv  25872  ubthlem1  26348  ubthlem2  26349  ubthlem3  26350  minvecolem1  26352  minvecolem4  26358  minvecolem5  26359  minvecolem6  26360  shel  26690  chel  26709  ocorth  26770  pjpreeq  26877  chscllem1  27116  chscllem2  27117  spansncvi  27131  off2  28073  xppreima  28079  ofpreima  28099  ofpreima2  28100  fcnvgreu  28106  1stpreimas  28117  infxrge0gelb  28178  supxrnemnf  28181  ssnnssfz  28194  iundisjfi  28199  hashunif  28207  toslublem  28257  tosglblem  28259  gsumvsca1  28375  gsumvsca2  28376  ress1r  28382  reff  28496  locfinreflem  28497  tpr2rico  28548  ordtrest2NEWlem  28558  ordtconlem1  28560  fsumcvg4  28586  indsum  28674  esummono  28705  esumpad  28706  esumpad2  28707  gsumesum  28710  esumrnmpt2  28719  esumsup  28740  esumgect  28741  esum2dlem  28743  esum2d  28744  esumiun  28745  elsigass  28777  elsigagen  28799  sigapildsys  28814  ldgenpisyslem1  28815  ldgenpisys  28818  measiuns  28869  measres  28874  volmeas  28884  omscl  28947  omssubadd  28952  carsguni  28960  carsggect  28970  carsgclctunlem2  28971  carsgclctunlem3  28972  omsmeas  28975  sibfof  28992  sitgclg  28994  sitgclbn  28995  eulerpartlemsv2  29008  eulerpartlemsf  29009  eulerpartlemsv3  29011  eulerpartlemgc  29012  eulerpartlemv  29014  eulerpartlemb  29018  eulerpartlemf  29020  eulerpartlemr  29024  eulerpartlemgvv  29026  eulerpartlemgu  29027  eulerpartlemgs2  29030  ballotlemsel1i  29162  ballotlemsima  29165  ballotlemfrceq  29178  signsplypnf  29218  signsply0  29219  signstcl  29233  signstf  29234  signstfvn  29237  signstfvp  29239  signsvfn  29250  bnj1137  29583  bnj1498  29649  erdszelem8  29700  cvmscld  29775  cvmsss2  29776  cvmopnlem  29780  cvmlift2lem9  29813  cvmlift2lem11  29815  cvmlift2lem12  29816  cvmliftpht  29820  mclsssvlem  29979  mclsppslem  30000  trpredelss  30251  sltres  30329  nobndup  30365  nobnddown  30366  nofulllem5  30371  opnrebl2  30753  fnessex  30778  fneuni  30779  neibastop1  30791  neibastop2lem  30792  neibastop3  30794  ptrecube  31634  poimirlem1  31635  poimirlem2  31636  poimirlem11  31645  poimirlem12  31646  poimirlem22  31656  poimirlem23  31657  poimirlem24  31658  poimirlem27  31661  poimirlem28  31662  poimirlem29  31663  opnmbllem0  31670  mblfinlem2  31672  ismblfin  31675  cnambfre  31683  itg2addnclem2  31688  ftc1cnnclem  31709  ftc1cnnc  31710  ftc1anclem6  31716  ftc1anclem7  31717  ftc1anclem8  31718  ftc1anc  31719  ftc2nc  31720  areacirclem2  31727  areacirclem4  31729  areacirc  31731  sdclem1  31766  mettrifi  31780  sstotbnd2  31800  equivtotbnd  31804  isbndx  31808  totbndbnd  31815  equivbnd2  31818  cntotbnd  31822  heibor1lem  31835  heiborlem3  31839  heibor  31847  iccbnd  31866  idlcl  31944  divrngidl  31955  lsatfixedN  32274  elpaddn0  33064  diaintclN  34325  dibglbN  34433  dibintclN  34434  dihrnlss  34544  dihglblem3N  34562  dihglblem6  34607  dihintcl  34611  dochkr1  34745  dochkr1OLDN  34746  lcfrlem5  34813  lcfr  34852  mapdrvallem2  34912  hgmapvvlem3  35195  hdmapoc  35201  hlhilocv  35227  ismrcd1  35239  mzpf  35277  mzpindd  35287  fphpdo  35359  pell14qrre  35401  pell14qrne0  35402  elpell14qr2  35406  elpell1qr2  35416  pellfundex  35430  dnnumch3lem  35600  dnnumch3  35601  fnwe2lem2  35605  aomclem4  35611  kelac1  35617  kercvrlsm  35637  hbtlem2  35679  hbtlem5  35683  flcidc  35729  cntzsdrg  35757  itgpowd  35788  areaquad  35790  radcnvrat  36290  binomcxplemdvbinom  36329  uzwo4  37023  wessf1ornlem  37072  ssfiunibd  37126  uzfissfz  37148  supxrgere  37155  supxrgelem  37159  supxrge  37160  suplesup  37161  iccshift  37194  iocopn  37196  eliccelioc  37197  iooshift  37198  icoiccdif  37200  icoopn  37201  fmul01  37220  fmulcl  37221  fprodexp  37236  fprodabs2  37237  climinf  37246  climinfOLD  37247  mullimc  37258  mullimcf  37265  idlimc  37268  limcperiod  37270  limcrecl  37271  limcresiooub  37285  limcresioolb  37286  limcleqr  37287  addlimc  37291  limclner  37294  cncfmptssg  37309  cncfshift  37313  cncfperiod  37318  cncfuni  37326  icccncfext  37327  dvmptidg  37349  dvbdfbdioolem1  37362  ioodvbdlimc1lem1  37365  dvmptfprodlem  37378  dvnprodlem1  37380  dvnprodlem2  37381  ibliccsinexp  37386  iblioosinexp  37388  itgcoscmulx  37405  itgsincmulx  37410  itgioocnicc  37413  itgiccshift  37416  itgperiod  37417  itgsbtaddcnst  37418  stoweidlem5  37424  stoweidlem11  37430  stoweidlem17  37436  stoweidlem18  37437  stoweidlem26  37445  stoweidlem27  37446  stoweidlem31  37451  stoweidlem35  37455  stoweidlem39  37459  stoweidlem42  37462  stoweidlem43  37463  stoweidlem44  37464  stoweidlem48  37468  stoweidlem51  37471  stoweidlem52  37472  stoweidlem56  37476  stoweidlem57  37477  stoweidlem59  37479  stoweidlem60  37480  stoweidlem61  37481  dirkeritg  37523  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem38  37566  fourierdlem39  37567  fourierdlem42  37570  fourierdlem46  37574  fourierdlem48  37576  fourierdlem49  37577  fourierdlem51  37579  fourierdlem53  37581  fourierdlem56  37584  fourierdlem57  37585  fourierdlem58  37586  fourierdlem64  37592  fourierdlem66  37594  fourierdlem68  37596  fourierdlem69  37597  fourierdlem70  37598  fourierdlem71  37599  fourierdlem72  37600  fourierdlem73  37601  fourierdlem74  37602  fourierdlem75  37603  fourierdlem76  37604  fourierdlem79  37607  fourierdlem80  37608  fourierdlem81  37609  fourierdlem83  37611  fourierdlem87  37615  fourierdlem90  37618  fourierdlem93  37621  fourierdlem95  37623  fourierdlem97  37625  fourierdlem101  37629  fourierdlem103  37631  fourierdlem104  37632  fourierdlem111  37639  fourierdlem112  37640  fourierdlem113  37641  fouriersw  37653  etransclem1  37657  etransclem4  37660  etransclem8  37664  etransclem17  37673  etransclem18  37674  etransclem20  37676  etransclem46  37702  intsaluni  37725  intsal  37726  sge0tsms  37746  sge0f1o  37748  sge0fsum  37753  sge0ltfirp  37766  sge0resplit  37772  sge0le  37773  sge0iunmptlemfi  37779  sge0iunmptlemre  37781  sge0fodjrnlem  37782  nnfoctbdjlem  37792  meadjiunlem  37802  ismeannd  37804  psmeasurelem  37807  iccpartres  38112  iccpartgt  38121  iccpartleu  38122  iccpartgel  38123  perfectALTVlem2  38224  bgoldbtbndlem2  38281  pfxf  38310  repswpfx  38357  elpwdifsn  38363  rhmsubclem3  38838  rhmsubclem4  38839  rhmsubcALTVlem4  38858  ssnn0ssfz  38880  lincresunit3  39024  fdivmptf  39103  refdivmptf  39104  elbigo2  39114
  Copyright terms: Public domain W3C validator