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

Theorem sselda 3180
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 3179 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 418 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684    C_ wss 3152
This theorem is referenced by:  elrel  4789  ffvresb  5690  1stdm  6167  oeeulem  6599  swoso  6691  erinxp  6733  boxcutc  6859  fundmen  6934  suplub2  7212  supisolem  7221  ordiso2  7230  ordtypelem2  7234  ordtypelem6  7238  ordtypelem7  7239  cantnflt  7373  cantnflem1c  7389  cantnflem1d  7390  cantnflem1  7391  cantnflem3  7393  cantnf  7395  cnfcomlem  7402  cnfcom3lem  7406  rankelb  7496  rankval3b  7498  ackbij2lem1  7845  ackbij1lem9  7854  ackbij1lem10  7855  ackbij1lem18  7863  ackbij2lem3  7867  ackbij2  7869  fin23lem7  7942  enfin2i  7947  isf32lem9  7987  isf34lem4  8003  fin1a2lem11  8036  hsmexlem4  8055  ttukeylem6  8141  fpwwe2lem8  8259  fpwwe2lem9  8260  fpwwe2  8265  canth4  8269  intwun  8357  wuncval2  8369  inttsk  8396  rankcf  8399  r1tskina  8404  tskuni  8405  elprnq  8615  suprub  9715  suprleub  9718  supmul1  9719  supmullem1  9720  supmul  9722  infmrgelb  9734  un0addcl  9997  un0mulcl  9998  suprzcl  10091  zsupss  10307  supxrleub  10645  supxrre  10646  supxrss  10651  infmxrgelb  10653  infmxrre  10654  icoshftf1o  10759  uzindi  11043  seqcl  11066  seqfveq  11070  monoord2  11077  sermono  11078  seqsplit  11079  seqcaopr2  11082  seqf1olem2a  11084  seqf1olem2  11086  seqhomo  11093  seqz  11094  seqcoll  11401  seqcoll2  11402  ccatval1  11431  ccatass  11436  revccat  11484  rexanre  11830  rexuzre  11836  rexico  11837  limsupgle  11951  limsupval2  11954  limsupgre  11955  limsupbnd2  11957  rlim2lt  11971  rlim3  11972  ello12  11990  lo1bdd2  11998  elo12  12001  rlimclim1  12019  climrlim2  12021  lo1resb  12038  o1resb  12040  rlimcn2  12064  o1of2  12086  rlimsqzlem  12122  isercolllem3  12140  isercoll2  12142  climsup  12143  iseraltlem2  12155  summolem2a  12188  sumss  12197  fsumss  12198  fsumcvg3  12202  fsumsplit  12212  fsum2dlem  12233  fsum0diag2  12245  fsumless  12254  fsumabs  12259  fsumtscopo  12260  fsumparts  12264  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  hashuni  12283  hashuniOLD  12284  ackbijnn  12286  binom1dif  12291  incexclem  12295  isumsplit  12299  isumrpcl  12302  isumless  12304  isumltss  12307  supcvg  12314  cvgrat  12339  mertenslem1  12340  rpnnen2  12504  bitsinv2  12634  bitsf1ocnv  12635  bitsinvp1  12640  eulerthlem2  12850  4sqlem11  13002  vdwlem6  13033  ramval  13055  ramcl2lem  13056  restid2  13335  mress  13495  mremre  13506  mreacs  13560  fullsubc  13724  subsubc  13727  funcres  13770  fuciso  13849  setcmon  13919  setcepi  13920  catccatid  13934  drsdirfi  14072  clatglbss  14231  ipodrsfi  14266  isacs3lem  14269  mrelatglb  14287  mrelatlub  14289  issubmnd  14401  gsumress  14454  gsumwspan  14468  frmdsssubm  14483  frmdss2  14485  subginv  14628  issubg2  14636  issubg4  14638  ssnmz  14659  lagsubg2  14678  resghm  14699  conjnmz  14716  conjnmzb  14717  subgga  14754  gass  14755  gasubg  14756  cntzsubm  14811  cntzmhm  14814  submod  14880  sylow1lem2  14910  sylow1lem3  14911  sylow1lem4  14912  sylow2alem2  14929  sylow2a  14930  sylow2blem2  14932  sylow3lem1  14938  sylow3lem6  14943  lsmssv  14954  lsmub2x  14958  lsmelvalm  14962  lsmcom2  14966  pj1lid  15010  pj1rid  15011  efgrelexlemb  15059  frgpup1  15084  frgpup3lem  15086  cntzcmn  15136  gsumval3eu  15190  gsumval3  15191  gsumzaddlem  15203  gsumzoppg  15216  dprdfadd  15255  dprdres  15263  dprdcntz2  15273  dprddisj2  15274  dprd2dlem1  15276  dmdprdsplit2lem  15280  ablfac1lem  15303  ablfac1b  15305  ablfac1c  15306  ablfac1eu  15308  pgpfac1lem1  15309  pgpfac1lem2  15310  pgpfac1lem3  15312  pgpfac1lem4  15313  ablfaclem3  15322  rngidss  15367  invrpropd  15480  subrg1  15555  subrginv  15561  subrgunit  15563  cntzsubr  15577  abvres  15604  lssel  15695  islss3  15716  lssintcl  15721  lmhmima  15804  lmhmpreima  15805  lbsel  15831  lbspropd  15852  lsmcv  15894  lspsolvlem  15895  lbsextlem2  15912  lidlsubcl  15968  drngnidl  15981  issubassa2  16084  mplcoe1  16209  mplcoe2  16211  subrgascl  16239  subrgasclcl  16240  zlpirlem1  16441  ocvocv  16571  ocvlss  16572  pjfo  16615  ocvpj  16617  obsne0  16625  obselocv  16628  tgclb  16708  tgidm  16718  pptbas  16745  toponmre  16830  clslp  16879  tgrest  16890  perfopn  16915  ordtbas  16922  ordtrest2lem  16933  pnrmcld  17070  ist1-3  17077  isreg2  17105  cncmp  17119  cmpsublem  17126  tgcmp  17128  cmpcld  17129  hauscmplem  17133  2ndcomap  17184  1stcelcls  17187  restlly  17209  lly1stc  17222  kgentopon  17233  llycmpkgen2  17245  txcls  17299  ptclsg  17309  txcnp  17314  txdis1cn  17329  txcmplem1  17335  txkgen  17346  xkoptsub  17348  xkopt  17349  xkococnlem  17353  xkoinjcn  17381  basqtop  17402  tgqtop  17403  kqfvima  17421  kqreglem1  17432  fbelss  17528  fbssfi  17532  fgabs  17574  trfg  17586  uffixfr  17618  uffixsn  17620  elfm2  17643  fmfnfmlem4  17652  fmfnfm  17653  flimnei  17662  flimrest  17678  flimcls  17680  flimsncls  17681  flffbas  17690  fclsrest  17719  fclscmp  17725  alexsublem  17738  ptcmplem3  17748  ptcmplem4  17749  subgntr  17789  opnsubg  17790  clssubg  17791  tgpconcomp  17795  divstgpopn  17802  divstgplem  17803  tsmssubm  17825  tgptsmscls  17832  tgptsmscld  17833  tsmsxplem1  17835  tsmsxplem2  17836  imasdsf1olem  17937  blpnfctr  17982  xmetresbl  17983  mopni2  18039  mopni3  18040  rnblopn  18045  tgioo  18302  xrsmopn  18318  zdis  18322  icccmplem3  18329  reconnlem2  18332  opnreen  18336  metdsf  18352  metdsge  18353  metdsle  18356  metdsre  18357  metnrmlem2  18364  metnrmlem3  18365  fsumcn  18374  climcncf  18404  icccvx  18448  cnheibor  18453  bndth  18456  lebnumlem1  18459  lebnumlem2  18460  pi1grplem  18547  clmneg  18579  nmoleub2lem3  18596  cphsqrcl  18620  cphabscl  18621  clsocv  18677  iscfil2  18692  cfil3i  18695  cfilfcls  18700  cmetcaulem  18714  iscmet3lem2  18718  cfilresi  18721  caussi  18723  lmclim  18728  minveclem1  18788  minveclem3b  18792  minveclem4  18796  minveclem6  18798  pjthlem2  18802  ivth2  18815  ivthicc  18818  ovollb2lem  18847  ovoliunlem1  18861  ovolicc2lem4  18879  ioombl1lem4  18918  dyadmax  18953  dyadmbl  18955  opnmbllem  18956  volsup2  18960  volivth  18962  vitalilem5  18967  i1fima  19033  i1fd  19036  itg1val2  19039  itg1cl  19040  itg1ge0  19041  itg11  19046  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  itg1mulc  19059  itg10a  19065  itg1ge0a  19066  itg1climres  19069  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1flim  19078  mbfmullem2  19079  itg2const2  19096  itg2splitlem  19103  itg2split  19104  itg2gt0  19115  itg2cnlem2  19117  iblss  19159  iblss2  19160  itgss3  19169  itgless  19171  itgfsum  19181  itgsplit  19190  itgsplitioo  19192  itggt0  19196  itgcn  19197  ditgcl  19208  ditgswap  19209  ditgsplitlem  19210  ellimc3  19229  perfdvf  19253  dvreslem  19259  dvcnp  19268  dvcnp2  19269  dvaddbr  19287  dvmulbr  19288  dvcjbr  19298  dvmptfsum  19322  dvcnvlem  19323  dvlip  19340  dvlipcn  19341  dvlip2  19342  dv11cn  19348  dvivthlem1  19355  dvivthlem2  19356  dvne0  19358  lhop1lem  19360  lhop2  19362  lhop  19363  dvcvx  19367  dvfsumle  19368  dvfsumge  19369  dvfsumabs  19370  dvfsumlem2  19374  dvfsumlem3  19375  dvfsumrlimge0  19377  dvfsumrlim2  19379  ftc1lem1  19382  ftc1lem4  19386  ftc1lem6  19388  itgsubstlem  19395  ig1peu  19557  plyeq0lem  19592  plypf1  19594  coeeulem  19606  vieta1lem1  19690  vieta1lem2  19691  plyexmo  19693  aaliou3lem2  19723  taylthlem1  19752  taylthlem2  19753  ulmdvlem1  19777  ulmdvlem3  19779  mtest  19781  radcnv0  19792  pserulm  19798  psercnlem2  19800  psercnlem1  19801  psercn  19802  pserdvlem1  19803  pserdvlem2  19804  pserdv  19805  pserdv2  19806  abelthlem3  19809  abelthlem4  19810  abelthlem9  19816  pige3  19885  efif1olem4  19907  efopnlem2  20004  efopn  20005  logccv  20010  loglesqr  20098  rlimcnp  20260  rlimcnp2  20261  xrlimcnp  20263  efrlim  20264  jensenlem1  20281  jensenlem2  20282  jensen  20283  fsumharmonic  20305  wilthlem2  20307  basellem3  20320  basellem5  20322  chtdif  20396  sqff1o  20420  musumsum  20432  muinv  20433  chtublem  20450  fsumvma  20452  vmasum  20455  chpval2  20457  chpchtsum  20458  chpub  20459  perfectlem2  20469  lgsquadlem2  20594  chebbnd1lem1  20618  dchrisumlem2  20639  dchrisumlem3  20640  dchrmusum2  20643  dchrisum0fno1  20660  rpvmasum2  20661  dchrisum0lem1b  20664  dchrisum0lem1  20665  rplogsum  20676  mudivsum  20679  mulogsum  20681  mulog2sumlem2  20684  selberg2lem  20699  chpdifbndlem1  20702  pntrlog2bndlem6  20732  pntrlog2bnd  20733  pntlemj  20752  pntlemf  20754  pntlem3  20758  subgoinv  20975  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  minvecolem1  21453  minvecolem4  21459  minvecolem5  21460  minvecolem6  21461  shel  21790  chel  21810  ocorth  21870  pjpreeq  21977  chscllem1  22216  chscllem2  22217  spansncvi  22231  ballotlemsel1i  23071  ballotlemfrceq  23087  off2  23208  xppreima  23211  tpr2rico  23296  hashunif  23385  elsigagen  23508  measiuns  23544  indsum  23606  erdszelem8  23729  cvmscld  23804  cvmsss2  23805  cvmopnlem  23809  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmliftpht  23849  umgraex  23875  eupares  23899  dedekind  24082  trpredelss  24235  sltres  24318  nobndup  24354  nobnddown  24355  nofulllem5  24360  axlowdimlem13  24582  axlowdimlem16  24585  axcontlem4  24595  axcontlem10  24601  bpolycl  24787  bpolysum  24788  bpolydiflem  24789  areacirclem4  24927  areacirclem5  24929  areacirc  24931  iscst4  25177  altretop  25600  lvsovso  25626  lvsovso2  25627  supnuf  25629  idsubfun  25858  vtarsuelt  25895  morexcmp  25967  opnrebl2  26236  fnessex  26275  fneuni  26276  comppfsc  26307  neibastop1  26308  neibastop2lem  26309  neibastop3  26311  sdclem1  26453  mettrifi  26473  sstotbnd2  26498  equivtotbnd  26502  isbndx  26506  totbndbnd  26513  equivbnd2  26516  cntotbnd  26520  heibor1lem  26533  heiborlem3  26537  heibor  26545  iccbnd  26564  idlcl  26642  divrngidl  26653  ismrcd1  26773  mzpf  26814  mzpindd  26824  fphpdo  26900  pell14qrre  26942  pell14qrne0  26943  elpell14qr2  26947  elpell1qr2  26957  pellfundex  26971  dnnumch3lem  27143  dnnumch3  27144  fnwe2lem2  27148  aomclem4  27154  kelac1  27161  kercvrlsm  27181  dsmmsubg  27209  frlmsslsp  27248  hbtlem2  27328  hbtlem5  27332  flcidc  27379  f1omvdmvd  27386  f1omvdconj  27389  symggen  27411  psgnunilem5  27417  psgnunilem2  27418  cntzsdrg  27510  climinf  27732  stoweidlem18  27767  stoweidlem26  27775  stoweidlem27  27776  stoweidlem31  27780  stoweidlem35  27784  stoweidlem39  27788  stoweidlem42  27791  stoweidlem48  27797  stoweidlem51  27800  stoweidlem56  27805  stoweidlem61  27810  bnj1137  29025  bnj1498  29091  lsatfixedN  29199  elpaddn0  29989  diaintclN  31248  dibglbN  31356  dibintclN  31357  dihrnlss  31467  dihglblem3N  31485  dihglblem6  31530  dihintcl  31534  dochkr1  31668  dochkr1OLDN  31669  lcfrlem5  31736  lcfr  31775  mapdrvallem2  31835  hgmapvvlem3  32118  hdmapoc  32124  hlhilocv  32150
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator