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

Theorem sselda 3350
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 3349 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 420 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726    C_ wss 3322
This theorem is referenced by:  elrel  4980  ffvresb  5902  1stdm  6396  oeeulem  6846  swoso  6938  erinxp  6980  boxcutc  7107  fundmen  7182  suplub2  7468  supisolem  7477  ordiso2  7486  ordtypelem2  7490  ordtypelem6  7494  ordtypelem7  7495  cantnflt  7629  cantnflem1c  7645  cantnflem1d  7646  cantnflem1  7647  cantnflem3  7649  cantnf  7651  cnfcomlem  7658  cnfcom3lem  7662  rankelb  7752  rankval3b  7754  ackbij2lem1  8101  ackbij1lem9  8110  ackbij1lem10  8111  ackbij1lem18  8119  ackbij2lem3  8123  ackbij2  8125  fin23lem7  8198  enfin2i  8203  isf32lem9  8243  isf34lem4  8259  fin1a2lem11  8292  hsmexlem4  8311  ttukeylem6  8396  fpwwe2lem8  8514  fpwwe2lem9  8515  fpwwe2  8520  canth4  8524  intwun  8612  wuncval2  8624  inttsk  8651  rankcf  8654  r1tskina  8659  tskuni  8660  elprnq  8870  suprub  9971  suprleub  9974  supmul1  9975  supmullem1  9976  supmul  9978  infmrgelb  9990  un0addcl  10255  un0mulcl  10256  suprzcl  10351  zsupss  10567  supxrleub  10907  supxrre  10908  supxrss  10913  infmxrgelb  10915  infmxrre  10916  icoshftf1o  11022  uzindi  11322  seqcl  11345  seqfveq  11349  monoord2  11356  sermono  11357  seqsplit  11358  seqcaopr2  11361  seqf1olem2a  11363  seqf1olem2  11365  seqhomo  11372  seqz  11373  seqof2  11383  seqcoll  11714  seqcoll2  11715  ccatval1  11747  ccatass  11752  revccat  11800  rexanre  12152  rexuzre  12158  rexico  12159  limsupgle  12273  limsupval2  12276  limsupgre  12277  limsupbnd2  12279  rlim2lt  12293  rlim3  12294  ello12  12312  lo1bdd2  12320  elo12  12323  rlimclim1  12341  climrlim2  12343  lo1resb  12360  o1resb  12362  rlimcn2  12386  o1of2  12408  rlimsqzlem  12444  isercolllem3  12462  isercoll2  12464  climsup  12465  iseraltlem2  12478  summolem2a  12511  sumss  12520  fsumss  12521  fsumcvg3  12525  fsumsplit  12535  fsum2dlem  12556  fsum0diag2  12568  fsumless  12577  fsumabs  12582  fsumtscopo  12583  fsumparts  12587  fsumrlim  12592  fsumo1  12593  o1fsum  12594  fsumiun  12602  hashuni  12606  hashuniOLD  12607  ackbijnn  12609  binom1dif  12614  incexclem  12618  isumsplit  12622  isumrpcl  12625  isumless  12627  isumltss  12630  supcvg  12637  cvgrat  12662  mertenslem1  12663  rpnnen2  12827  bitsinv2  12957  bitsf1ocnv  12958  bitsinvp1  12963  eulerthlem2  13173  4sqlem11  13325  vdwlem6  13356  ramval  13378  ramcl2lem  13379  restid2  13660  mress  13820  mremre  13831  mreacs  13885  fullsubc  14049  subsubc  14052  funcres  14095  fuciso  14174  setcmon  14244  setcepi  14245  catccatid  14259  drsdirfi  14397  clatglbss  14556  ipodrsfi  14591  isacs3lem  14594  mrelatglb  14612  mrelatlub  14614  issubmnd  14726  gsumress  14779  gsumwspan  14793  frmdsssubm  14808  frmdss2  14810  subginv  14953  issubg2  14961  issubg4  14963  ssnmz  14984  lagsubg2  15003  resghm  15024  conjnmz  15041  conjnmzb  15042  subgga  15079  gass  15080  gasubg  15081  cntzsubm  15136  cntzmhm  15139  submod  15205  sylow1lem2  15235  sylow1lem3  15236  sylow1lem4  15237  sylow2alem2  15254  sylow2a  15255  sylow2blem2  15257  sylow3lem1  15263  sylow3lem6  15268  lsmssv  15279  lsmub2x  15283  lsmelvalm  15287  lsmcom2  15291  pj1lid  15335  pj1rid  15336  efgrelexlemb  15384  frgpup1  15409  frgpup3lem  15411  cntzcmn  15461  gsumval3eu  15515  gsumval3  15516  gsumzaddlem  15528  gsumzoppg  15541  dprdfadd  15580  dprdres  15588  dprdcntz2  15598  dprddisj2  15599  dprd2dlem1  15601  dmdprdsplit2lem  15605  ablfac1lem  15628  ablfac1b  15630  ablfac1c  15631  ablfac1eu  15633  pgpfac1lem1  15634  pgpfac1lem2  15635  pgpfac1lem3  15637  pgpfac1lem4  15638  ablfaclem3  15647  rngidss  15692  invrpropd  15805  subrg1  15880  subrginv  15886  subrgunit  15888  cntzsubr  15902  abvres  15929  lssel  16016  islss3  16037  lssintcl  16042  lmhmima  16125  lmhmpreima  16126  lbsel  16152  lbspropd  16173  lsmcv  16215  lspsolvlem  16216  lbsextlem2  16233  lidlsubcl  16289  drngnidl  16302  issubassa2  16405  mplcoe1  16530  mplcoe2  16532  subrgascl  16560  subrgasclcl  16561  zlpirlem1  16770  ocvocv  16900  ocvlss  16901  pjfo  16944  ocvpj  16946  obsne0  16954  obselocv  16957  tgclb  17037  tgidm  17047  pptbas  17074  toponmre  17159  neiptoptop  17197  neiptopnei  17198  neiptopreu  17199  clslp  17214  tgrest  17225  perfopn  17251  ordtbas  17258  ordtrest2lem  17269  pnrmcld  17408  ist1-3  17415  isreg2  17443  cncmp  17457  cmpsublem  17464  tgcmp  17466  cmpcld  17467  hauscmplem  17471  2ndcomap  17523  1stcelcls  17526  restlly  17548  lly1stc  17561  kgentopon  17572  llycmpkgen2  17584  txcls  17638  ptclsg  17649  txcnp  17654  txdis1cn  17669  txcmplem1  17675  txkgen  17686  xkoptsub  17688  xkopt  17689  xkococnlem  17693  xkoinjcn  17721  basqtop  17745  tgqtop  17746  kqfvima  17764  kqreglem1  17775  fbelss  17867  fbssfi  17871  fgabs  17913  trfg  17925  uffixfr  17957  uffixsn  17959  elfm2  17982  fmfnfmlem4  17991  fmfnfm  17992  flimnei  18001  flimrest  18017  flimcls  18019  flimsncls  18020  flffbas  18029  fclsrest  18058  fclscmp  18064  alexsublem  18077  ptcmplem3  18087  ptcmplem4  18088  cnextfres  18101  subgntr  18138  opnsubg  18139  clssubg  18140  tgpconcomp  18144  divstgpopn  18151  divstgplem  18152  tsmssubm  18174  tgptsmscls  18181  tgptsmscld  18182  tsmsxplem1  18184  tsmsxplem2  18185  ustssxp  18236  ustuqtop4  18276  utopsnneiplem  18279  utop2nei  18282  isucn2  18311  ucnima  18313  psmetres2  18347  imasdsf1olem  18405  blpnfctr  18468  xmetresbl  18469  mopni2  18525  mopni3  18526  rnblopn  18531  metustexhalfOLD  18595  metustexhalf  18596  metutopOLD  18614  psmetutop  18615  tgioo  18829  xrsmopn  18845  zdis  18849  icccmplem3  18857  reconnlem2  18860  opnreen  18864  metdsf  18880  metdsge  18881  metdsle  18884  metdsre  18885  metnrmlem2  18892  metnrmlem3  18893  fsumcn  18902  climcncf  18932  icccvx  18977  cnheibor  18982  bndth  18985  lebnumlem1  18988  lebnumlem2  18989  pi1grplem  19076  clmneg  19108  nmoleub2lem3  19125  cphsqrcl  19149  cphabscl  19150  clsocv  19206  iscfil2  19221  cfil3i  19224  cfilfcls  19229  cmetcaulem  19243  iscmet3lem2  19247  cfilresi  19250  caussi  19252  lmclim  19257  minveclem1  19327  minveclem3b  19331  minveclem4  19335  minveclem6  19337  pjthlem2  19341  ivth2  19354  ivthicc  19357  ovollb2lem  19386  ovoliunlem1  19400  ovolicc2lem4  19418  ioombl1lem4  19457  dyadmax  19492  dyadmbl  19494  opnmbllem  19495  volsup2  19499  volivth  19501  vitalilem5  19506  i1fima  19572  i1fd  19575  itg1val2  19578  itg1cl  19579  itg1ge0  19580  itg11  19585  i1fadd  19589  i1fmul  19590  itg1addlem4  19593  itg1addlem5  19594  i1fmulc  19597  itg1mulc  19598  itg10a  19604  itg1ge0a  19605  itg1climres  19608  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  mbfi1flim  19617  mbfmullem2  19618  itg2const2  19635  itg2splitlem  19642  itg2split  19643  itg2gt0  19654  itg2cnlem2  19656  iblss  19698  iblss2  19699  itgss3  19708  itgless  19710  itgfsum  19720  itgsplit  19729  itgsplitioo  19731  itggt0  19735  itgcn  19736  ditgcl  19747  ditgswap  19748  ditgsplitlem  19749  ellimc3  19768  perfdvf  19792  dvreslem  19798  dvcnp  19807  dvcnp2  19808  dvaddbr  19826  dvmulbr  19827  dvcjbr  19837  dvmptfsum  19861  dvcnvlem  19862  dvlip  19879  dvlipcn  19880  dvlip2  19881  dv11cn  19887  dvivthlem1  19894  dvivthlem2  19895  dvne0  19897  lhop1lem  19899  lhop2  19901  lhop  19902  dvcvx  19906  dvfsumle  19907  dvfsumge  19908  dvfsumabs  19909  dvfsumlem2  19913  dvfsumlem3  19914  dvfsumrlimge0  19916  dvfsumrlim2  19918  ftc1lem1  19921  ftc1lem4  19925  ftc1lem6  19927  itgsubstlem  19934  ig1peu  20096  plyeq0lem  20131  plypf1  20133  coeeulem  20145  vieta1lem1  20229  vieta1lem2  20230  plyexmo  20232  aaliou3lem2  20262  taylthlem1  20291  taylthlem2  20292  ulmdvlem1  20318  ulmdvlem3  20320  mtest  20322  radcnv0  20334  pserulm  20340  psercnlem2  20342  psercnlem1  20343  psercn  20344  pserdvlem1  20345  pserdvlem2  20346  pserdv  20347  pserdv2  20348  abelthlem3  20351  abelthlem4  20352  abelthlem9  20358  pige3  20427  efif1olem4  20449  efopnlem2  20550  efopn  20551  logccv  20556  loglesqr  20644  rlimcnp  20806  rlimcnp2  20807  xrlimcnp  20809  efrlim  20810  jensenlem1  20827  jensenlem2  20828  jensen  20829  fsumharmonic  20852  wilthlem2  20854  basellem3  20867  basellem5  20869  chtdif  20943  sqff1o  20967  musumsum  20979  muinv  20980  chtublem  20997  fsumvma  20999  vmasum  21002  chpval2  21004  chpchtsum  21005  chpub  21006  perfectlem2  21016  lgsquadlem2  21141  chebbnd1lem1  21165  dchrisumlem2  21186  dchrisumlem3  21187  dchrmusum2  21190  dchrisum0fno1  21207  rpvmasum2  21208  dchrisum0lem1b  21211  dchrisum0lem1  21212  rplogsum  21223  mudivsum  21226  mulogsum  21228  mulog2sumlem2  21231  selberg2lem  21246  chpdifbndlem1  21249  pntrlog2bndlem6  21279  pntrlog2bnd  21280  pntlemj  21299  pntlemf  21301  pntlem3  21305  umgraex  21360  redwlk  21608  eupares  21699  subgoinv  21898  ubthlem1  22374  ubthlem2  22375  ubthlem3  22376  minvecolem1  22378  minvecolem4  22384  minvecolem5  22385  minvecolem6  22386  shel  22715  chel  22735  ocorth  22795  pjpreeq  22902  chscllem1  23141  chscllem2  23142  spansncvi  23156  off2  24056  xppreima  24061  ofpreima  24083  supxrnemnf  24129  ssnnssfz  24150  iundisjfi  24154  hashunif  24160  ress0g  24184  toslub  24193  tosglb  24194  tpr2rico  24312  indsum  24422  esummono  24452  gsumesum  24453  elsigass  24510  elsigagen  24532  measiuns  24573  measres  24578  volmeas  24589  sibfof  24656  sitgclg  24658  ballotlemsel1i  24772  ballotlemsima  24775  ballotlemfrceq  24788  lgamgulmlem2  24816  lgamgulm2  24822  lgambdd  24823  erdszelem8  24886  cvmscld  24962  cvmsss2  24963  cvmopnlem  24967  cvmlift2lem9  25000  cvmlift2lem11  25002  cvmlift2lem12  25003  cvmliftpht  25007  dedekind  25189  clim2prod  25218  prodfn0  25224  prodfrec  25225  prodmolem2a  25262  fprodntriv  25270  prodss  25275  fprodss  25276  fprodsplit  25291  fprod2dlem  25306  binomfallfaclem2  25358  trpredelss  25512  sltres  25621  nobndup  25657  nobnddown  25658  nofulllem5  25663  axlowdimlem13  25895  axlowdimlem16  25898  axcontlem4  25908  axcontlem10  25914  bpolycl  26100  bpolysum  26101  bpolydiflem  26102  supaddc  26239  supadd  26240  opnmbllem0  26244  mblfinlem2  26246  ismblfin  26249  cnambfre  26257  itg2addnclem2  26259  ftc1cnnclem  26280  ftc1cnnc  26281  ftc1anclem6  26287  ftc1anclem7  26288  ftc1anclem8  26289  ftc1anc  26290  ftc2nc  26291  areacirclem2  26295  areacirclem4  26297  areacirc  26299  opnrebl2  26326  fnessex  26357  fneuni  26358  comppfsc  26389  neibastop1  26390  neibastop2lem  26391  neibastop3  26393  sdclem1  26449  mettrifi  26465  sstotbnd2  26485  equivtotbnd  26489  isbndx  26493  totbndbnd  26500  equivbnd2  26503  cntotbnd  26507  heibor1lem  26520  heiborlem3  26524  heibor  26532  iccbnd  26551  idlcl  26629  divrngidl  26640  ismrcd1  26754  mzpf  26795  mzpindd  26805  fphpdo  26880  pell14qrre  26922  pell14qrne0  26923  elpell14qr2  26927  elpell1qr2  26937  pellfundex  26951  dnnumch3lem  27123  dnnumch3  27124  fnwe2lem2  27128  aomclem4  27134  kelac1  27140  kercvrlsm  27160  dsmmsubg  27188  frlmsslsp  27227  hbtlem2  27307  hbtlem5  27311  flcidc  27358  f1omvdmvd  27365  f1omvdconj  27368  symggen  27390  psgnunilem5  27396  psgnunilem2  27397  cntzsdrg  27489  fmul01  27688  fmulcl  27689  climinf  27710  ibliccsinexp  27723  iblioosinexp  27725  stoweidlem5  27732  stoweidlem7  27734  stoweidlem11  27738  stoweidlem17  27744  stoweidlem18  27745  stoweidlem26  27753  stoweidlem27  27754  stoweidlem31  27758  stoweidlem35  27762  stoweidlem39  27766  stoweidlem42  27769  stoweidlem43  27770  stoweidlem44  27771  stoweidlem48  27775  stoweidlem51  27778  stoweidlem52  27779  stoweidlem56  27783  stoweidlem57  27784  stoweidlem59  27786  stoweidlem60  27787  stoweidlem61  27788  swrd0swrd  28219  swrdccatin2lem1  28228  bnj1137  29426  bnj1498  29492  lsatfixedN  29869  elpaddn0  30659  diaintclN  31918  dibglbN  32026  dibintclN  32027  dihrnlss  32137  dihglblem3N  32155  dihglblem6  32200  dihintcl  32204  dochkr1  32338  dochkr1OLDN  32339  lcfrlem5  32406  lcfr  32445  mapdrvallem2  32505  hgmapvvlem3  32788  hdmapoc  32794  hlhilocv  32820
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator