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

Theorem sselda 3454
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 3453 . 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 1758    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  elrel  5040  ffvresb  5973  1stdm  6721  tfrlem1  6935  oeeulem  7140  swoso  7232  erinxp  7274  boxcutc  7406  fundmen  7483  suplub2  7812  supisolem  7821  ordiso2  7830  ordtypelem2  7834  ordtypelem6  7838  ordtypelem7  7839  cantnflt  7981  cantnflem1c  7996  cantnflem1d  7997  cantnflem1  7998  cantnflem3  8000  cantnf  8002  cantnfltOLD  8011  cantnflem1cOLD  8019  cantnflem1dOLD  8020  cantnflem1OLD  8021  cantnflem3OLD  8022  cantnfOLD  8024  cnfcomlem  8033  cnfcom3lem  8037  cnfcomlemOLD  8041  cnfcom3lemOLD  8045  rankelb  8132  rankval3b  8134  ackbij2lem1  8489  ackbij1lem9  8498  ackbij1lem10  8499  ackbij1lem18  8507  ackbij2lem3  8511  ackbij2  8513  fin23lem7  8586  enfin2i  8591  isf32lem9  8631  isf34lem4  8647  fin1a2lem11  8680  hsmexlem4  8699  ttukeylem6  8784  fpwwe2lem8  8905  fpwwe2lem9  8906  fpwwe2  8911  canth4  8915  intwun  9003  wuncval2  9015  inttsk  9042  rankcf  9045  r1tskina  9050  tskuni  9051  elprnq  9261  dedekind  9634  suprub  10392  suprleub  10395  supmul1  10396  supmullem1  10397  supmul  10399  infmrgelb  10411  un0addcl  10714  un0mulcl  10715  suprzcl  10822  zsupss  11045  supxrleub  11390  supxrre  11391  supxrss  11396  infmxrgelb  11398  infmxrre  11399  icoshftf1o  11509  supicc  11534  supiccub  11535  supicclub  11536  supicclub2  11537  uzindi  11904  seqcl  11927  seqfveq  11931  monoord2  11938  sermono  11939  seqsplit  11940  seqcaopr2  11943  seqf1olem2a  11945  seqf1olem2  11947  seqhomo  11954  seqz  11955  seqof2  11965  seqcoll  12318  seqcoll2  12319  ccatval1  12378  ccatass  12388  revccat  12508  rexanre  12936  rexuzre  12942  rexico  12943  limsupgle  13057  limsupval2  13060  limsupgre  13061  limsupbnd2  13063  rlim2lt  13077  rlim3  13078  ello12  13096  lo1bdd2  13104  elo12  13107  rlimclim1  13125  climrlim2  13127  lo1resb  13144  o1resb  13146  rlimcn2  13170  o1of2  13192  rlimsqzlem  13228  isercolllem3  13246  isercoll2  13248  climsup  13249  iseraltlem2  13262  summolem2a  13294  sumss  13303  fsumss  13304  fsumcvg3  13308  fsumsplit  13318  fsum2dlem  13339  fsum0diag2  13352  fsumless  13361  fsumabs  13366  fsumtscopo  13367  fsumparts  13371  fsumrlim  13376  fsumo1  13377  o1fsum  13378  fsumiun  13386  hashuni  13390  hashuniOLD  13391  ackbijnn  13393  binom1dif  13398  incexclem  13401  isumsplit  13405  isumrpcl  13408  isumless  13410  isumltss  13413  supcvg  13420  cvgrat  13445  mertenslem1  13446  rpnnen2  13610  bitsinv2  13741  bitsf1ocnv  13742  bitsinvp1  13747  eulerthlem2  13959  4sqlem11  14118  vdwlem6  14149  ramval  14171  ramcl2lem  14172  restid2  14471  mress  14633  mremre  14644  mreacs  14698  fullsubc  14862  subsubc  14865  funcres  14908  fuciso  14987  setcmon  15057  setcepi  15058  catccatid  15072  drsdirfi  15210  clatglbss  15399  ipodrsfi  15435  isacs3lem  15438  mrelatglb  15456  mrelatlub  15458  issubmnd  15551  ress0g  15552  gsumress  15609  gsumwspan  15626  frmdsssubm  15641  frmdss2  15643  grpinvssd  15705  subginv  15790  issubg2  15798  issubg4  15802  ssnmz  15825  lagsubg2  15844  resghm  15865  conjnmz  15882  conjnmzb  15883  subgga  15920  gass  15921  gasubg  15922  cntzsubm  15955  cntzmhm  15958  f1omvdmvd  16051  f1omvdconj  16054  symggen  16078  psgnunilem5  16102  psgnunilem2  16103  submod  16172  sylow1lem2  16202  sylow1lem3  16203  sylow1lem4  16204  sylow2alem2  16221  sylow2a  16222  sylow2blem2  16224  sylow3lem1  16230  sylow3lem6  16235  lsmssv  16246  lsmub2x  16250  lsmelvalm  16254  lsmcom2  16258  pj1lid  16302  pj1rid  16303  efgrelexlemb  16351  frgpup1  16376  frgpup3lem  16378  cntzcmn  16428  gsumval3eu  16485  gsumval3OLD  16486  gsumval3  16489  gsumzaddlem  16512  gsumzaddlemOLD  16514  gsumzoppg  16545  gsumzoppgOLD  16546  dprdfadd  16615  dprdfaddOLD  16622  dprdres  16630  dprdcntz2  16641  dprddisj2  16642  dprddisj2OLD  16643  dprd2dlem1  16645  dmdprdsplit2lem  16649  ablfac1lem  16674  ablfac1b  16676  ablfac1c  16677  ablfac1eu  16679  pgpfac1lem1  16680  pgpfac1lem2  16681  pgpfac1lem3  16683  pgpfac1lem4  16684  ablfaclem3  16693  rngidss  16777  invrpropd  16896  subrg1  16981  subrginv  16987  subrgunit  16989  cntzsubr  17003  abvres  17030  lssel  17125  islss3  17146  lssintcl  17151  lmhmima  17234  lmhmpreima  17235  lbsel  17265  lbspropd  17286  lsmcv  17328  lspsolvlem  17329  lbsextlem2  17346  lidlsubcl  17404  drngnidl  17417  issubassa2  17521  mplcoe1  17651  mplcoe5lem  17654  mplcoe5  17655  mplcoe2OLD  17657  subrgascl  17687  subrgasclcl  17688  zringlpirlem1  18012  zlpirlem1  18017  regsumsupp  18161  ocvocv  18205  ocvlss  18206  pjfo  18249  ocvpj  18251  obsne0  18259  obselocv  18262  dsmmsubg  18277  frlmsslsp  18332  frlmsslspOLD  18333  ofco2  18443  mdetrsca2  18526  mdetunilem9  18542  madugsum  18565  tgclb  18691  tgidm  18701  pptbas  18728  toponmre  18813  neiptoptop  18851  neiptopnei  18852  neiptopreu  18853  clslp  18868  tgrest  18879  perfopn  18905  ordtbas  18912  ordtrest2lem  18923  pnrmcld  19062  ist1-3  19069  isreg2  19097  cncmp  19111  cmpsublem  19118  tgcmp  19120  cmpcld  19121  hauscmplem  19125  2ndcomap  19178  1stcelcls  19181  restlly  19203  lly1stc  19216  kgentopon  19227  llycmpkgen2  19239  txcls  19293  ptclsg  19304  txcnp  19309  txdis1cn  19324  txcmplem1  19330  txkgen  19341  xkoptsub  19343  xkopt  19344  xkococnlem  19348  xkoinjcn  19376  basqtop  19400  tgqtop  19401  kqfvima  19419  kqreglem1  19430  fbelss  19522  fbssfi  19526  fgabs  19568  trfg  19580  uffixfr  19612  uffixsn  19614  elfm2  19637  fmfnfmlem4  19646  fmfnfm  19647  flimnei  19656  flimrest  19672  flimcls  19674  flimsncls  19675  flffbas  19684  fclsrest  19713  fclscmp  19719  alexsublem  19732  ptcmplem3  19742  ptcmplem4  19743  cnextfres  19756  subgntr  19793  opnsubg  19794  clssubg  19795  tgpconcomp  19799  divstgpopn  19806  divstgplem  19807  tsmssubm  19832  tgptsmscls  19840  tgptsmscld  19841  tsmsxplem1  19843  tsmsxplem2  19844  ustssxp  19895  ustuqtop4  19935  utopsnneiplem  19938  utop2nei  19941  isucn2  19970  ucnima  19972  psmetres2  20006  imasdsf1olem  20064  blpnfctr  20127  xmetresbl  20128  mopni2  20184  mopni3  20185  rnblopn  20190  metustexhalfOLD  20254  metustexhalf  20255  metutopOLD  20273  psmetutop  20274  tgioo  20489  xrsmopn  20505  zdis  20509  icccmplem3  20517  reconnlem2  20520  opnreen  20524  metdsf  20540  metdsge  20541  metdsle  20544  metdsre  20545  metnrmlem2  20552  metnrmlem3  20553  fsumcn  20562  climcncf  20592  icccvx  20638  cnheibor  20643  bndth  20646  lebnumlem1  20649  lebnumlem2  20650  pi1grplem  20737  clmneg  20769  nmoleub2lem3  20786  cphsqrcl  20819  cphabscl  20820  clsocv  20878  iscfil2  20893  cfil3i  20896  cfilfcls  20901  cmetcaulem  20915  iscmet3lem2  20919  cfilresi  20922  caussi  20924  lmclim  20929  rrxnm  21011  rrxcph  21012  rrxmval  21020  rrxmetlem  21022  rrxmet  21023  rrxdstprj1  21024  minveclem1  21027  minveclem3b  21031  minveclem4  21035  minveclem6  21037  pjthlem2  21041  ivth2  21055  ivthicc  21058  ovollb2lem  21087  ovoliunlem1  21101  ovolicc2lem4  21119  ioombl1lem4  21158  dyadmax  21194  dyadmbl  21196  opnmbllem  21197  volsup2  21201  volivth  21203  vitalilem5  21208  i1fima  21272  i1fd  21275  itg1val2  21278  itg1cl  21279  itg1ge0  21280  itg11  21285  i1fadd  21289  i1fmul  21290  itg1addlem4  21293  itg1addlem5  21294  i1fmulc  21297  itg1mulc  21298  itg10a  21304  itg1ge0a  21305  itg1climres  21308  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfi1flim  21317  mbfmullem2  21318  itg2const2  21335  itg2splitlem  21342  itg2split  21343  itg2gt0  21354  itg2cnlem2  21356  iblss  21398  iblss2  21399  itgss3  21408  itgless  21410  itgfsum  21420  itgsplit  21429  itgsplitioo  21431  itggt0  21435  itgcn  21436  ditgcl  21449  ditgswap  21450  ditgsplitlem  21451  ellimc3  21470  perfdvf  21494  dvreslem  21500  dvcnp  21509  dvcnp2  21510  dvaddbr  21528  dvmulbr  21529  dvcjbr  21539  dvmptfsum  21563  dvcnvlem  21564  dvlip  21581  dvlipcn  21582  dvlip2  21583  dv11cn  21589  dvivthlem1  21596  dvivthlem2  21597  dvne0  21599  lhop1lem  21601  lhop2  21603  lhop  21604  dvcvx  21608  dvfsumle  21609  dvfsumge  21610  dvfsumabs  21611  dvfsumlem2  21615  dvfsumlem3  21616  dvfsumrlimge0  21618  dvfsumrlim2  21620  ftc1lem1  21623  ftc1lem4  21627  ftc1lem6  21629  itgsubstlem  21636  ig1peu  21759  plyeq0lem  21794  plypf1  21796  coeeulem  21808  vieta1lem1  21892  vieta1lem2  21893  plyexmo  21895  taylthlem1  21954  taylthlem2  21955  ulmdvlem1  21981  ulmdvlem3  21983  mtest  21985  radcnv0  21997  pserulm  22003  psercnlem2  22005  psercnlem1  22006  psercn  22007  pserdvlem1  22008  pserdvlem2  22009  pserdv  22010  pserdv2  22011  abelthlem3  22014  abelthlem4  22015  abelthlem9  22021  pige3  22095  efif1olem4  22117  efopnlem2  22218  efopn  22219  logccv  22224  loglesqr  22312  rlimcnp  22475  rlimcnp2  22476  xrlimcnp  22478  efrlim  22479  jensenlem1  22496  jensenlem2  22497  jensen  22498  fsumharmonic  22521  wilthlem2  22523  basellem3  22536  basellem5  22538  chtdif  22612  sqff1o  22636  musumsum  22648  muinv  22649  chtublem  22666  fsumvma  22668  vmasum  22671  chpval2  22673  chpchtsum  22674  chpub  22675  perfectlem2  22685  lgsquadlem2  22810  chebbnd1lem1  22834  dchrisumlem2  22855  dchrisumlem3  22856  dchrmusum2  22859  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0lem1b  22880  dchrisum0lem1  22881  rplogsum  22892  mudivsum  22895  mulogsum  22897  mulog2sumlem2  22900  selberg2lem  22915  chpdifbndlem1  22918  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntlemj  22968  pntlemf  22970  pntlem3  22974  tglineelsb2  23160  tglinecom  23163  axlowdimlem13  23335  axlowdimlem16  23338  axcontlem4  23348  axcontlem10  23354  umgraex  23392  redwlk  23640  eupares  23731  subgoinv  23930  ubthlem1  24406  ubthlem2  24407  ubthlem3  24408  minvecolem1  24410  minvecolem4  24416  minvecolem5  24417  minvecolem6  24418  shel  24748  chel  24768  ocorth  24829  pjpreeq  24936  chscllem1  25175  chscllem2  25176  spansncvi  25190  off2  26093  xppreima  26098  ofpreima  26118  ofpreima2  26119  fcnvgreu  26125  supxrnemnf  26190  ssnnssfz  26210  iundisjfi  26214  hashunif  26218  toslublem  26262  tosglblem  26264  gsumvsca1  26385  gsumvsca2  26386  ress1r  26391  tpr2rico  26476  ordtrest2NEWlem  26486  ordtconlem1  26488  fsumcvg4  26514  indsum  26613  esummono  26643  gsumesum  26644  elsigass  26702  elsigagen  26724  measiuns  26765  measres  26770  volmeas  26781  sibfof  26860  sitgclg  26862  eulerpartlemsv2  26875  eulerpartlemsf  26876  eulerpartlemsv3  26878  eulerpartlemgc  26879  eulerpartlemv  26881  eulerpartlemb  26885  eulerpartlemf  26887  eulerpartlemr  26891  eulerpartlemgvv  26893  eulerpartlemgu  26894  eulerpartlemgs2  26897  ballotlemsel1i  27029  ballotlemsima  27032  ballotlemfrceq  27045  signsplypnf  27085  signsply0  27086  signstcl  27100  signstf  27101  signstfvn  27104  signstfvp  27106  signsvfn  27117  lgamgulmlem2  27150  lgamgulm2  27156  lgambdd  27157  erdszelem8  27220  cvmscld  27296  cvmsss2  27297  cvmopnlem  27301  cvmlift2lem9  27334  cvmlift2lem11  27336  cvmlift2lem12  27337  cvmliftpht  27341  clim2prod  27537  prodfn0  27543  prodfrec  27544  prodmolem2a  27581  fprodntriv  27589  prodss  27594  fprodss  27595  fprodsplit  27610  fprod2dlem  27625  binomfallfaclem2  27677  trpredelss  27830  sltres  27939  nobndup  27975  nobnddown  27976  nofulllem5  27981  bpolycl  28329  bpolysum  28330  bpolydiflem  28331  supaddc  28555  supadd  28556  opnmbllem0  28565  mblfinlem2  28567  ismblfin  28570  cnambfre  28578  itg2addnclem2  28582  ftc1cnnclem  28603  ftc1cnnc  28604  ftc1anclem6  28610  ftc1anclem7  28611  ftc1anclem8  28612  ftc1anc  28613  ftc2nc  28614  areacirclem2  28623  areacirclem4  28625  areacirc  28627  opnrebl2  28654  fnessex  28685  fneuni  28686  comppfsc  28717  neibastop1  28718  neibastop2lem  28719  neibastop3  28721  sdclem1  28777  mettrifi  28791  sstotbnd2  28811  equivtotbnd  28815  isbndx  28819  totbndbnd  28826  equivbnd2  28829  cntotbnd  28833  heibor1lem  28846  heiborlem3  28850  heibor  28858  iccbnd  28877  idlcl  28955  divrngidl  28966  ismrcd1  29172  mzpf  29210  mzpindd  29220  fphpdo  29294  pell14qrre  29336  pell14qrne0  29337  elpell14qr2  29341  elpell1qr2  29351  pellfundex  29365  dnnumch3lem  29537  dnnumch3  29538  fnwe2lem2  29542  aomclem4  29548  kelac1  29554  kercvrlsm  29574  hbtlem2  29618  hbtlem5  29622  flcidc  29669  cntzsdrg  29697  itgpowd  29728  areaquad  29730  fmul01  29899  fmulcl  29900  climinf  29917  ibliccsinexp  29929  iblioosinexp  29931  stoweidlem5  29938  stoweidlem11  29944  stoweidlem17  29950  stoweidlem18  29951  stoweidlem26  29959  stoweidlem27  29960  stoweidlem31  29964  stoweidlem35  29968  stoweidlem39  29972  stoweidlem42  29975  stoweidlem43  29976  stoweidlem44  29977  stoweidlem48  29981  stoweidlem51  29984  stoweidlem52  29985  stoweidlem56  29989  stoweidlem57  29990  stoweidlem59  29992  stoweidlem60  29993  stoweidlem61  29994  elfzom1elfzo  30355  zpnn0elfzo  30359  wwlkm1edg  30505  clwlkisclwwlklem2fv1  30582  clwlkisclwwlklem1  30587  clwwlkvbij  30601  clwwisshclwwlem  30608  clwlkfclwwlk  30655  ssnn0ssfz  30879  lincresunit3  31122  bnj1137  32286  bnj1498  32352  lsatfixedN  32960  elpaddn0  33750  diaintclN  35009  dibglbN  35117  dibintclN  35118  dihrnlss  35228  dihglblem3N  35246  dihglblem6  35291  dihintcl  35295  dochkr1  35429  dochkr1OLDN  35430  lcfrlem5  35497  lcfr  35536  mapdrvallem2  35596  hgmapvvlem3  35879  hdmapoc  35885  hlhilocv  35911
  Copyright terms: Public domain W3C validator