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

Theorem sselda 3417
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 3416 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 427 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1826    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  elrel  5018  ffvresb  5964  1stdm  6746  tfrlem1  6963  oeeulem  7168  swoso  7260  erinxp  7303  boxcutc  7431  fundmen  7508  suplub2  7835  supisolem  7846  ordiso2  7855  ordtypelem2  7859  ordtypelem6  7863  ordtypelem7  7864  cantnflt  8004  cantnflem1c  8019  cantnflem1d  8020  cantnflem1  8021  cantnflem3  8023  cantnf  8025  cantnfltOLD  8034  cantnflem1cOLD  8042  cantnflem1dOLD  8043  cantnflem1OLD  8044  cantnflem3OLD  8045  cantnfOLD  8047  cnfcomlem  8056  cnfcom3lem  8060  cnfcomlemOLD  8064  cnfcom3lemOLD  8068  rankelb  8155  rankval3b  8157  ackbij2lem1  8512  ackbij1lem9  8521  ackbij1lem10  8522  ackbij1lem18  8530  ackbij2lem3  8534  ackbij2  8536  fin23lem7  8609  enfin2i  8614  isf32lem9  8654  isf34lem4  8670  fin1a2lem11  8703  hsmexlem4  8722  ttukeylem6  8807  fpwwe2lem8  8926  fpwwe2lem9  8927  fpwwe2  8932  canth4  8936  intwun  9024  wuncval2  9036  inttsk  9063  rankcf  9066  r1tskina  9071  tskuni  9072  elprnq  9280  dedekind  9655  suprub  10420  suprleub  10423  supmul1  10424  supmullem1  10425  supmul  10427  infmrgelb  10439  un0addcl  10746  un0mulcl  10747  suprzcl  10859  zsupss  11090  supxrleub  11439  supxrre  11440  supxrss  11445  infmxrgelb  11447  infmxrre  11448  icoshftf1o  11564  supicc  11589  supiccub  11590  supicclub  11591  supicclub2  11592  elfzoext  11772  elfzom1elfzo  11783  zpnn0elfzo  11787  uzindi  11994  seqcl  12030  seqfveq  12034  monoord2  12041  sermono  12042  seqsplit  12043  seqcaopr2  12046  seqf1olem2a  12048  seqf1olem2  12050  seqhomo  12057  seqz  12058  seqof2  12068  seqcoll  12416  seqcoll2  12417  ccatass  12514  ccatrn  12515  revccat  12651  rexanre  13181  rexuzre  13187  rexico  13188  limsupgle  13302  limsupval2  13305  limsupgre  13306  limsupbnd2  13308  rlim2lt  13322  rlim3  13323  ello12  13341  lo1bdd2  13349  elo12  13352  rlimclim1  13370  climrlim2  13372  lo1resb  13389  o1resb  13391  rlimcn2  13415  o1of2  13437  rlimsqzlem  13473  isercolllem3  13491  isercoll2  13493  climsup  13494  iseraltlem2  13507  summolem2a  13539  sumss  13548  fsumss  13549  fsumcvg3  13553  fsumsplit  13564  fsum2dlem  13587  fsum0diag2  13600  fsumless  13612  fsumabs  13617  telfsumo  13618  fsumparts  13622  fsumrlim  13627  fsumo1  13628  o1fsum  13629  fsumiun  13637  hashuni  13640  ackbijnn  13642  binom1dif  13647  incexclem  13650  isumsplit  13654  isumrpcl  13657  isumless  13659  isumltss  13662  supcvg  13669  cvgrat  13694  mertenslem1  13695  clim2prod  13699  prodfn0  13705  prodfrec  13706  prodmolem2a  13743  fprodntriv  13751  prodss  13756  fprodss  13757  fprodsplit  13772  fprod2dlem  13786  rpnnen2  13961  bitsinv2  14095  bitsf1ocnv  14096  bitsinvp1  14101  eulerthlem2  14314  4sqlem11  14475  vdwlem6  14506  ramval  14528  ramcl2lem  14529  restid2  14838  mress  15000  mremre  15011  mreacs  15065  fullsubc  15256  subsubc  15259  funcres  15302  fuciso  15381  initoeu2lem1  15410  initoeu2  15412  setcmon  15483  setcepi  15484  catccatid  15498  drsdirfi  15684  clatglbss  15874  ipodrsfi  15910  isacs3lem  15913  mrelatglb  15931  mrelatlub  15933  gsumress  16020  issubmnd  16065  ress0g  16066  gsumwspan  16131  frmdsssubm  16146  frmdss2  16148  grpinvssd  16232  subginv  16325  issubg2  16333  issubg4  16337  ssnmz  16360  lagsubg2  16379  resghm  16400  conjnmz  16417  conjnmzb  16418  subgga  16455  gass  16456  gasubg  16457  cntzsubm  16490  cntzmhm  16493  f1omvdmvd  16585  f1omvdconj  16588  symggen  16612  psgnunilem5  16636  psgnunilem2  16637  submod  16706  sylow1lem2  16736  sylow1lem3  16737  sylow1lem4  16738  sylow2alem2  16755  sylow2a  16756  sylow2blem2  16758  sylow3lem1  16764  sylow3lem6  16769  lsmssv  16780  lsmub2x  16784  lsmelvalm  16788  lsmcom2  16792  pj1lid  16836  pj1rid  16837  efgrelexlemb  16885  frgpup1  16910  frgpup3lem  16912  cntzcmn  16965  gsumval3eu  17024  gsumval3OLD  17025  gsumval3  17028  gsumzaddlem  17051  gsumzaddlemOLD  17053  gsumzoppg  17083  gsumzoppgOLD  17084  dprdfadd  17173  dprdfaddOLD  17180  dprdres  17188  dprdcntz2  17199  dprddisj2  17200  dprddisj2OLD  17201  dprd2dlem1  17203  dmdprdsplit2lem  17207  ablfac1lem  17232  ablfac1b  17234  ablfac1c  17235  ablfac1eu  17237  pgpfac1lem1  17238  pgpfac1lem2  17239  pgpfac1lem3  17241  pgpfac1lem4  17242  ablfaclem3  17251  ringidss  17338  invrpropd  17460  subrg1  17552  subrginv  17558  subrgunit  17560  cntzsubr  17574  abvres  17601  lssel  17697  islss3  17718  lssintcl  17723  lmhmima  17806  lmhmpreima  17807  lbsel  17837  lbspropd  17858  lsmcv  17900  lspsolvlem  17901  lbsextlem2  17918  lidlsubclOLD  17977  drngnidl  17990  issubassa2  18107  mplcoe1  18240  mplcoe5lem  18243  mplcoe5  18244  mplcoe2OLD  18246  subrgascl  18276  subrgasclcl  18277  zringlpirlem1  18615  regsumsupp  18749  ocvocv  18793  ocvlss  18794  pjfo  18837  ocvpj  18839  obsne0  18847  obselocv  18850  dsmmsubg  18865  frlmsslsp  18916  ofco2  19038  mdetrsca2  19191  mdetunilem9  19207  madugsum  19230  tgclb  19557  tgidm  19567  pptbas  19594  toponmre  19680  neiptoptop  19718  neiptopnei  19719  neiptopreu  19720  clslp  19735  tgrest  19746  perfopn  19772  ordtbas  19779  ordtrest2lem  19790  pnrmcld  19929  ist1-3  19936  isreg2  19964  cncmp  19978  cmpsublem  19985  tgcmp  19987  cmpcld  19988  hauscmplem  19992  2ndcomap  20044  1stcelcls  20047  restlly  20069  lly1stc  20082  comppfsc  20118  kgentopon  20124  llycmpkgen2  20136  txcls  20190  ptclsg  20201  txcnp  20206  txdis1cn  20221  txcmplem1  20227  txkgen  20238  xkoptsub  20240  xkopt  20241  xkococnlem  20245  xkoinjcn  20273  basqtop  20297  tgqtop  20298  kqfvima  20316  kqreglem1  20327  fbelss  20419  fbssfi  20423  fgabs  20465  trfg  20477  uffixfr  20509  uffixsn  20511  elfm2  20534  fmfnfmlem4  20543  fmfnfm  20544  flimnei  20553  flimrest  20569  flimcls  20571  flimsncls  20572  flffbas  20581  fclsrest  20610  fclscmp  20616  alexsublem  20629  ptcmplem3  20639  ptcmplem4  20640  cnextfres  20653  subgntr  20690  opnsubg  20691  clssubg  20692  tgpconcomp  20696  qustgpopn  20703  qustgplem  20704  tsmssubm  20729  tgptsmscls  20737  tgptsmscld  20738  tsmsxplem1  20740  tsmsxplem2  20741  ustssxp  20792  ustuqtop4  20832  utopsnneiplem  20835  utop2nei  20838  isucn2  20867  ucnima  20869  psmetres2  20903  imasdsf1olem  20961  blpnfctr  21024  xmetresbl  21025  mopni2  21081  mopni3  21082  rnblopn  21087  metustexhalfOLD  21151  metustexhalf  21152  metutopOLD  21170  psmetutop  21171  tgioo  21386  xrsmopn  21402  zdis  21406  icccmplem3  21414  reconnlem2  21417  opnreen  21421  metdsf  21437  metdsge  21438  metdsle  21441  metdsre  21442  metnrmlem2  21449  metnrmlem3  21450  fsumcn  21459  climcncf  21489  icccvx  21535  cnheibor  21540  bndth  21543  lebnumlem1  21546  lebnumlem2  21547  pi1grplem  21634  clmneg  21666  nmoleub2lem3  21683  cphsqrtcl  21716  cphabscl  21717  clsocv  21775  iscfil2  21790  cfil3i  21793  cfilfcls  21798  cmetcaulem  21812  iscmet3lem2  21816  cfilresi  21819  caussi  21821  lmclim  21826  rrxnm  21908  rrxcph  21909  rrxmval  21917  rrxmetlem  21919  rrxmet  21920  rrxdstprj1  21921  minveclem1  21924  minveclem3b  21928  minveclem4  21932  minveclem6  21934  pjthlem2  21938  ivth2  21952  ivthicc  21955  ovollb2lem  21984  ovoliunlem1  21998  ovolicc2lem4  22016  ioombl1lem4  22056  dyadmax  22092  dyadmbl  22094  opnmbllem  22095  volsup2  22099  volivth  22101  vitalilem5  22106  i1fima  22170  i1fd  22173  itg1val2  22176  itg1cl  22177  itg1ge0  22178  itg11  22183  i1fadd  22187  i1fmul  22188  itg1addlem4  22191  itg1addlem5  22192  i1fmulc  22195  itg1mulc  22196  itg10a  22202  itg1ge0a  22203  itg1climres  22206  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  mbfi1flim  22215  mbfmullem2  22216  itg2const2  22233  itg2splitlem  22240  itg2split  22241  itg2gt0  22252  itg2cnlem2  22254  iblss  22296  iblss2  22297  itgss3  22306  itgless  22308  itgfsum  22318  itgsplit  22327  itgsplitioo  22329  itggt0  22333  itgcn  22334  ditgcl  22347  ditgswap  22348  ditgsplitlem  22349  ellimc3  22368  perfdvf  22392  dvreslem  22398  dvcnp  22407  dvcnp2  22408  dvaddbr  22426  dvmulbr  22427  dvcjbr  22437  dvmptfsum  22461  dvcnvlem  22462  dvlip  22479  dvlipcn  22480  dvlip2  22481  dv11cn  22487  dvivthlem1  22494  dvivthlem2  22495  dvne0  22497  lhop1lem  22499  lhop2  22501  lhop  22502  dvcvx  22506  dvfsumle  22507  dvfsumge  22508  dvfsumabs  22509  dvfsumlem2  22513  dvfsumlem3  22514  dvfsumrlimge0  22516  dvfsumrlim2  22518  ftc1lem1  22521  ftc1lem4  22525  ftc1lem6  22527  itgsubstlem  22534  ig1peu  22657  plyeq0lem  22692  plypf1  22694  coeeulem  22706  vieta1lem1  22791  vieta1lem2  22792  plyexmo  22794  taylthlem1  22853  taylthlem2  22854  ulmdvlem1  22880  ulmdvlem3  22882  mtest  22884  radcnv0  22896  pserulm  22902  psercnlem2  22904  psercnlem1  22905  psercn  22906  pserdvlem1  22907  pserdvlem2  22908  pserdv  22909  pserdv2  22910  abelthlem3  22913  abelthlem4  22914  abelthlem9  22920  pige3  22995  efif1olem4  23017  efabl  23022  efsubm  23023  efopnlem2  23125  efopn  23126  logccv  23131  loglesqrt  23219  rlimcnp  23412  rlimcnp2  23413  xrlimcnp  23415  efrlim  23416  jensenlem1  23433  jensenlem2  23434  jensen  23435  fsumharmonic  23458  wilthlem2  23460  basellem3  23473  basellem5  23475  chtdif  23549  sqff1o  23573  musumsum  23585  muinv  23586  chtublem  23603  fsumvma  23605  vmasum  23608  chpval2  23610  chpchtsum  23611  chpub  23612  perfectlem2  23622  lgsquadlem2  23747  chebbnd1lem1  23771  dchrisumlem2  23792  dchrisumlem3  23793  dchrmusum2  23796  dchrisum0fno1  23813  rpvmasum2  23814  dchrisum0lem1b  23817  dchrisum0lem1  23818  rplogsum  23829  mudivsum  23832  mulogsum  23834  mulog2sumlem2  23837  selberg2lem  23852  chpdifbndlem1  23855  pntrlog2bndlem6  23885  pntrlog2bnd  23886  pntlemj  23905  pntlemf  23907  pntlem3  23911  tglineelsb2  24132  tglinecom  24135  axlowdimlem13  24378  axlowdimlem16  24381  axcontlem4  24391  axcontlem10  24397  umgraex  24444  edg  24474  redwlk  24729  wwlkm1edg  24856  clwlkisclwwlklem2fv1  24903  clwlkisclwwlklem1  24908  clwwlkvbij  24922  clwwisshclwwlem  24927  clwlkfclwwlk  24965  eupares  25096  subgoinv  25427  ubthlem1  25903  ubthlem2  25904  ubthlem3  25905  minvecolem1  25907  minvecolem4  25913  minvecolem5  25914  minvecolem6  25915  shel  26245  chel  26265  ocorth  26326  pjpreeq  26433  chscllem1  26672  chscllem2  26673  spansncvi  26687  off2  27621  xppreima  27627  ofpreima  27653  ofpreima2  27654  fcnvgreu  27660  1stpreimas  27671  supxrnemnf  27736  ssnnssfz  27750  iundisjfi  27754  hashunif  27758  toslublem  27808  tosglblem  27810  gsumvsca1  27927  gsumvsca2  27928  ress1r  27933  reff  27996  locfinreflem  27997  tpr2rico  28048  ordtrest2NEWlem  28058  ordtconlem1  28060  fsumcvg4  28086  indsum  28171  esummono  28202  esumpad  28203  esumpad2  28204  gsumesum  28207  esumrnmpt2  28216  esumsup  28237  esumgect  28238  esum2dlem  28240  esum2d  28241  esumiun  28242  elsigass  28274  elsigagen  28296  sigapildsys  28307  measiuns  28344  measres  28349  volmeas  28359  omscl  28422  omssubadd  28427  carsguni  28435  carsggect  28445  carsgclctunlem2  28446  carsgclctunlem3  28447  omsmeas  28450  sibfof  28465  sitgclg  28467  sitgclbn  28468  eulerpartlemsv2  28480  eulerpartlemsf  28481  eulerpartlemsv3  28483  eulerpartlemgc  28484  eulerpartlemv  28486  eulerpartlemb  28490  eulerpartlemf  28492  eulerpartlemr  28496  eulerpartlemgvv  28498  eulerpartlemgu  28499  eulerpartlemgs2  28502  ballotlemsel1i  28634  ballotlemsima  28637  ballotlemfrceq  28650  signsplypnf  28690  signsply0  28691  signstcl  28705  signstf  28706  signstfvn  28709  signstfvp  28711  signsvfn  28722  lgamgulmlem2  28761  lgamgulm2  28767  lgambdd  28768  erdszelem8  28831  cvmscld  28907  cvmsss2  28908  cvmopnlem  28912  cvmlift2lem9  28945  cvmlift2lem11  28947  cvmlift2lem12  28948  cvmliftpht  28952  mclsssvlem  29111  mclsppslem  29132  binomfallfaclem2  29328  trpredelss  29480  sltres  29589  nobndup  29625  nobnddown  29626  nofulllem5  29631  bpolycl  29967  bpolysum  29968  bpolydiflem  29969  supaddc  30206  supadd  30207  opnmbllem0  30215  mblfinlem2  30217  ismblfin  30220  cnambfre  30228  itg2addnclem2  30233  ftc1cnnclem  30254  ftc1cnnc  30255  ftc1anclem6  30261  ftc1anclem7  30262  ftc1anclem8  30263  ftc1anc  30264  ftc2nc  30265  areacirclem2  30274  areacirclem4  30276  areacirc  30278  opnrebl2  30305  fnessex  30330  fneuni  30331  neibastop1  30343  neibastop2lem  30344  neibastop3  30346  sdclem1  30402  mettrifi  30416  sstotbnd2  30436  equivtotbnd  30440  isbndx  30444  totbndbnd  30451  equivbnd2  30454  cntotbnd  30458  heibor1lem  30471  heiborlem3  30475  heibor  30483  iccbnd  30502  idlcl  30580  divrngidl  30591  ismrcd1  30796  mzpf  30834  mzpindd  30844  fphpdo  30916  pell14qrre  30958  pell14qrne0  30959  elpell14qr2  30963  elpell1qr2  30973  pellfundex  30987  dnnumch3lem  31158  dnnumch3  31159  fnwe2lem2  31163  aomclem4  31169  kelac1  31175  kercvrlsm  31195  hbtlem2  31241  hbtlem5  31245  flcidc  31291  cntzsdrg  31319  itgpowd  31350  areaquad  31352  radcnvrat  31363  binomcxplemdvbinom  31426  infmxrss  31658  ssfiunibd  31675  iccshift  31724  iocopn  31726  eliccelioc  31727  iooshift  31728  icoiccdif  31730  icoopn  31731  fmul01  31740  fmulcl  31741  fprodexp  31766  fprodabs2  31768  climinf  31778  mullimc  31788  mullimcf  31795  idlimc  31798  limcperiod  31800  limcrecl  31801  limcresiooub  31814  limcresioolb  31815  limcleqr  31816  addlimc  31820  limclner  31823  cncfmptssg  31838  cncfshift  31842  cncfperiod  31847  cncfuni  31855  icccncfext  31856  dvmptidg  31878  dvbdfbdioolem1  31891  ioodvbdlimc1lem1  31894  dvmptfprodlem  31907  dvnprodlem1  31909  dvnprodlem2  31910  ibliccsinexp  31915  iblioosinexp  31917  itgcoscmulx  31934  itgsincmulx  31939  itgioocnicc  31942  itgiccshift  31945  itgperiod  31946  itgsbtaddcnst  31947  stoweidlem5  31953  stoweidlem11  31959  stoweidlem17  31965  stoweidlem18  31966  stoweidlem26  31974  stoweidlem27  31975  stoweidlem31  31979  stoweidlem35  31983  stoweidlem39  31987  stoweidlem42  31990  stoweidlem43  31991  stoweidlem44  31992  stoweidlem48  31996  stoweidlem51  31999  stoweidlem52  32000  stoweidlem56  32004  stoweidlem57  32005  stoweidlem59  32007  stoweidlem60  32008  stoweidlem61  32009  dirkeritg  32050  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem38  32093  fourierdlem39  32094  fourierdlem42  32097  fourierdlem46  32101  fourierdlem48  32103  fourierdlem49  32104  fourierdlem51  32106  fourierdlem53  32108  fourierdlem56  32111  fourierdlem57  32112  fourierdlem58  32113  fourierdlem64  32119  fourierdlem66  32121  fourierdlem68  32123  fourierdlem69  32124  fourierdlem70  32125  fourierdlem71  32126  fourierdlem72  32127  fourierdlem73  32128  fourierdlem74  32129  fourierdlem75  32130  fourierdlem76  32131  fourierdlem79  32134  fourierdlem80  32135  fourierdlem81  32136  fourierdlem83  32138  fourierdlem87  32142  fourierdlem90  32145  fourierdlem93  32148  fourierdlem95  32150  fourierdlem97  32152  fourierdlem101  32156  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem112  32167  fourierdlem113  32168  fouriersw  32180  etransclem1  32184  etransclem4  32187  etransclem8  32191  etransclem17  32200  etransclem18  32201  etransclem20  32203  etransclem46  32229  perfectALTVlem2  32544  pfxf  32564  repswpfx  32611  elpwdifsn  32617  rhmsubclem3  33096  rhmsubclem4  33097  rhmsubcALTVlem4  33116  ssnn0ssfz  33138  lincresunit3  33282  fdivmptf  33362  refdivmptf  33363  elbigo2  33373  bnj1137  34398  bnj1498  34464  lsatfixedN  35147  elpaddn0  35937  diaintclN  37198  dibglbN  37306  dibintclN  37307  dihrnlss  37417  dihglblem3N  37435  dihglblem6  37480  dihintcl  37484  dochkr1  37618  dochkr1OLDN  37619  lcfrlem5  37686  lcfr  37725  mapdrvallem2  37785  hgmapvvlem3  38068  hdmapoc  38074  hlhilocv  38100
  Copyright terms: Public domain W3C validator