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

Theorem sselda 3256
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 3255 . 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 1710    C_ wss 3228
This theorem is referenced by:  elrel  4871  ffvresb  5773  1stdm  6254  oeeulem  6686  swoso  6778  erinxp  6820  boxcutc  6947  fundmen  7022  suplub2  7302  supisolem  7311  ordiso2  7320  ordtypelem2  7324  ordtypelem6  7328  ordtypelem7  7329  cantnflt  7463  cantnflem1c  7479  cantnflem1d  7480  cantnflem1  7481  cantnflem3  7483  cantnf  7485  cnfcomlem  7492  cnfcom3lem  7496  rankelb  7586  rankval3b  7588  ackbij2lem1  7935  ackbij1lem9  7944  ackbij1lem10  7945  ackbij1lem18  7953  ackbij2lem3  7957  ackbij2  7959  fin23lem7  8032  enfin2i  8037  isf32lem9  8077  isf34lem4  8093  fin1a2lem11  8126  hsmexlem4  8145  ttukeylem6  8231  fpwwe2lem8  8349  fpwwe2lem9  8350  fpwwe2  8355  canth4  8359  intwun  8447  wuncval2  8459  inttsk  8486  rankcf  8489  r1tskina  8494  tskuni  8495  elprnq  8705  suprub  9805  suprleub  9808  supmul1  9809  supmullem1  9810  supmul  9812  infmrgelb  9824  un0addcl  10089  un0mulcl  10090  suprzcl  10183  zsupss  10399  supxrleub  10737  supxrre  10738  supxrss  10743  infmxrgelb  10745  infmxrre  10746  icoshftf1o  10851  uzindi  11135  seqcl  11158  seqfveq  11162  monoord2  11169  sermono  11170  seqsplit  11171  seqcaopr2  11174  seqf1olem2a  11176  seqf1olem2  11178  seqhomo  11185  seqz  11186  seqof2  11196  seqcoll  11497  seqcoll2  11498  ccatval1  11527  ccatass  11532  revccat  11580  rexanre  11926  rexuzre  11932  rexico  11933  limsupgle  12047  limsupval2  12050  limsupgre  12051  limsupbnd2  12053  rlim2lt  12067  rlim3  12068  ello12  12086  lo1bdd2  12094  elo12  12097  rlimclim1  12115  climrlim2  12117  lo1resb  12134  o1resb  12136  rlimcn2  12160  o1of2  12182  rlimsqzlem  12218  isercolllem3  12236  isercoll2  12238  climsup  12239  iseraltlem2  12252  summolem2a  12285  sumss  12294  fsumss  12295  fsumcvg3  12299  fsumsplit  12309  fsum2dlem  12330  fsum0diag2  12342  fsumless  12351  fsumabs  12356  fsumtscopo  12357  fsumparts  12361  fsumrlim  12366  fsumo1  12367  o1fsum  12368  fsumiun  12376  hashuni  12380  hashuniOLD  12381  ackbijnn  12383  binom1dif  12388  incexclem  12392  isumsplit  12396  isumrpcl  12399  isumless  12401  isumltss  12404  supcvg  12411  cvgrat  12436  mertenslem1  12437  rpnnen2  12601  bitsinv2  12731  bitsf1ocnv  12732  bitsinvp1  12737  eulerthlem2  12947  4sqlem11  13099  vdwlem6  13130  ramval  13152  ramcl2lem  13153  restid2  13434  mress  13594  mremre  13605  mreacs  13659  fullsubc  13823  subsubc  13826  funcres  13869  fuciso  13948  setcmon  14018  setcepi  14019  catccatid  14033  drsdirfi  14171  clatglbss  14330  ipodrsfi  14365  isacs3lem  14368  mrelatglb  14386  mrelatlub  14388  issubmnd  14500  gsumress  14553  gsumwspan  14567  frmdsssubm  14582  frmdss2  14584  subginv  14727  issubg2  14735  issubg4  14737  ssnmz  14758  lagsubg2  14777  resghm  14798  conjnmz  14815  conjnmzb  14816  subgga  14853  gass  14854  gasubg  14855  cntzsubm  14910  cntzmhm  14913  submod  14979  sylow1lem2  15009  sylow1lem3  15010  sylow1lem4  15011  sylow2alem2  15028  sylow2a  15029  sylow2blem2  15031  sylow3lem1  15037  sylow3lem6  15042  lsmssv  15053  lsmub2x  15057  lsmelvalm  15061  lsmcom2  15065  pj1lid  15109  pj1rid  15110  efgrelexlemb  15158  frgpup1  15183  frgpup3lem  15185  cntzcmn  15235  gsumval3eu  15289  gsumval3  15290  gsumzaddlem  15302  gsumzoppg  15315  dprdfadd  15354  dprdres  15362  dprdcntz2  15372  dprddisj2  15373  dprd2dlem1  15375  dmdprdsplit2lem  15379  ablfac1lem  15402  ablfac1b  15404  ablfac1c  15405  ablfac1eu  15407  pgpfac1lem1  15408  pgpfac1lem2  15409  pgpfac1lem3  15411  pgpfac1lem4  15412  ablfaclem3  15421  rngidss  15466  invrpropd  15579  subrg1  15654  subrginv  15660  subrgunit  15662  cntzsubr  15676  abvres  15703  lssel  15794  islss3  15815  lssintcl  15820  lmhmima  15903  lmhmpreima  15904  lbsel  15930  lbspropd  15951  lsmcv  15993  lspsolvlem  15994  lbsextlem2  16011  lidlsubcl  16067  drngnidl  16080  issubassa2  16183  mplcoe1  16308  mplcoe2  16310  subrgascl  16338  subrgasclcl  16339  zlpirlem1  16547  ocvocv  16677  ocvlss  16678  pjfo  16721  ocvpj  16723  obsne0  16731  obselocv  16734  tgclb  16814  tgidm  16824  pptbas  16851  toponmre  16936  clslp  16985  tgrest  16996  perfopn  17021  ordtbas  17028  ordtrest2lem  17039  pnrmcld  17176  ist1-3  17183  isreg2  17211  cncmp  17225  cmpsublem  17232  tgcmp  17234  cmpcld  17235  hauscmplem  17239  2ndcomap  17290  1stcelcls  17293  restlly  17315  lly1stc  17328  kgentopon  17339  llycmpkgen2  17351  txcls  17405  ptclsg  17415  txcnp  17420  txdis1cn  17435  txcmplem1  17441  txkgen  17452  xkoptsub  17454  xkopt  17455  xkococnlem  17459  xkoinjcn  17487  basqtop  17508  tgqtop  17509  kqfvima  17527  kqreglem1  17538  fbelss  17630  fbssfi  17634  fgabs  17676  trfg  17688  uffixfr  17720  uffixsn  17722  elfm2  17745  fmfnfmlem4  17754  fmfnfm  17755  flimnei  17764  flimrest  17780  flimcls  17782  flimsncls  17783  flffbas  17792  fclsrest  17821  fclscmp  17827  alexsublem  17840  ptcmplem3  17850  ptcmplem4  17851  subgntr  17891  opnsubg  17892  clssubg  17893  tgpconcomp  17897  divstgpopn  17904  divstgplem  17905  tsmssubm  17927  tgptsmscls  17934  tgptsmscld  17935  tsmsxplem1  17937  tsmsxplem2  17938  imasdsf1olem  18039  blpnfctr  18084  xmetresbl  18085  mopni2  18141  mopni3  18142  rnblopn  18147  tgioo  18404  xrsmopn  18420  zdis  18424  icccmplem3  18432  reconnlem2  18435  opnreen  18439  metdsf  18455  metdsge  18456  metdsle  18459  metdsre  18460  metnrmlem2  18467  metnrmlem3  18468  fsumcn  18477  climcncf  18507  icccvx  18552  cnheibor  18557  bndth  18560  lebnumlem1  18563  lebnumlem2  18564  pi1grplem  18651  clmneg  18683  nmoleub2lem3  18700  cphsqrcl  18724  cphabscl  18725  clsocv  18781  iscfil2  18796  cfil3i  18799  cfilfcls  18804  cmetcaulem  18818  iscmet3lem2  18822  cfilresi  18825  caussi  18827  lmclim  18832  minveclem1  18892  minveclem3b  18896  minveclem4  18900  minveclem6  18902  pjthlem2  18906  ivth2  18919  ivthicc  18922  ovollb2lem  18951  ovoliunlem1  18965  ovolicc2lem4  18983  ioombl1lem4  19022  dyadmax  19057  dyadmbl  19059  opnmbllem  19060  volsup2  19064  volivth  19066  vitalilem5  19071  i1fima  19137  i1fd  19140  itg1val2  19143  itg1cl  19144  itg1ge0  19145  itg11  19150  i1fadd  19154  i1fmul  19155  itg1addlem4  19158  itg1addlem5  19159  i1fmulc  19162  itg1mulc  19163  itg10a  19169  itg1ge0a  19170  itg1climres  19173  mbfi1fseqlem4  19177  mbfi1fseqlem5  19178  mbfi1flim  19182  mbfmullem2  19183  itg2const2  19200  itg2splitlem  19207  itg2split  19208  itg2gt0  19219  itg2cnlem2  19221  iblss  19263  iblss2  19264  itgss3  19273  itgless  19275  itgfsum  19285  itgsplit  19294  itgsplitioo  19296  itggt0  19300  itgcn  19301  ditgcl  19312  ditgswap  19313  ditgsplitlem  19314  ellimc3  19333  perfdvf  19357  dvreslem  19363  dvcnp  19372  dvcnp2  19373  dvaddbr  19391  dvmulbr  19392  dvcjbr  19402  dvmptfsum  19426  dvcnvlem  19427  dvlip  19444  dvlipcn  19445  dvlip2  19446  dv11cn  19452  dvivthlem1  19459  dvivthlem2  19460  dvne0  19462  lhop1lem  19464  lhop2  19466  lhop  19467  dvcvx  19471  dvfsumle  19472  dvfsumge  19473  dvfsumabs  19474  dvfsumlem2  19478  dvfsumlem3  19479  dvfsumrlimge0  19481  dvfsumrlim2  19483  ftc1lem1  19486  ftc1lem4  19490  ftc1lem6  19492  itgsubstlem  19499  ig1peu  19661  plyeq0lem  19696  plypf1  19698  coeeulem  19710  vieta1lem1  19794  vieta1lem2  19795  plyexmo  19797  aaliou3lem2  19827  taylthlem1  19856  taylthlem2  19857  ulmdvlem1  19883  ulmdvlem3  19885  mtest  19887  mtestbdd  19888  radcnv0  19899  pserulm  19905  psercnlem2  19907  psercnlem1  19908  psercn  19909  pserdvlem1  19910  pserdvlem2  19911  pserdv  19912  pserdv2  19913  abelthlem3  19916  abelthlem4  19917  abelthlem9  19923  pige3  19992  efif1olem4  20014  efopnlem2  20115  efopn  20116  logccv  20121  loglesqr  20209  rlimcnp  20371  rlimcnp2  20372  xrlimcnp  20374  efrlim  20375  jensenlem1  20392  jensenlem2  20393  jensen  20394  fsumharmonic  20417  wilthlem2  20419  basellem3  20432  basellem5  20434  chtdif  20508  sqff1o  20532  musumsum  20544  muinv  20545  chtublem  20562  fsumvma  20564  vmasum  20567  chpval2  20569  chpchtsum  20570  chpub  20571  perfectlem2  20581  lgsquadlem2  20706  chebbnd1lem1  20730  dchrisumlem2  20751  dchrisumlem3  20752  dchrmusum2  20755  dchrisum0fno1  20772  rpvmasum2  20773  dchrisum0lem1b  20776  dchrisum0lem1  20777  rplogsum  20788  mudivsum  20791  mulogsum  20793  mulog2sumlem2  20796  selberg2lem  20811  chpdifbndlem1  20814  pntrlog2bndlem6  20844  pntrlog2bnd  20845  pntlemj  20864  pntlemf  20866  pntlem3  20870  subgoinv  21087  ubthlem1  21563  ubthlem2  21564  ubthlem3  21565  minvecolem1  21567  minvecolem4  21573  minvecolem5  21574  minvecolem6  21575  shel  21904  chel  21924  ocorth  21984  pjpreeq  22091  chscllem1  22330  chscllem2  22331  spansncvi  22345  off2  23258  xppreima  23262  hashunif  23362  ress0g  23387  neiptopnei  23445  neiptopreu  23446  tpr2rico  23466  ustssxp  23510  ustrel  23517  ustuqtop4  23548  utopsnneiplem  23551  ucnima  23576  metutop  23611  indsum  23686  esummono  23716  gsumesum  23717  elsigagen  23796  measiuns  23835  volmeas  23851  ballotlemsel1i  24019  ballotlemfrceq  24035  lgamgulmlem2  24063  lgamgulm2  24069  lgambdd  24070  erdszelem8  24133  cvmscld  24208  cvmsss2  24209  cvmopnlem  24213  cvmlift2lem9  24246  cvmlift2lem11  24248  cvmlift2lem12  24249  cvmliftpht  24253  umgraex  24279  eupares  24303  dedekind  24488  clim2prod  24517  prodfn0  24523  prodfrec  24524  prodmolem2a  24561  fprodntriv  24569  prodss  24574  fprodss  24575  fprodsplit  24590  trpredelss  24793  sltres  24876  nobndup  24912  nobnddown  24913  nofulllem5  24918  axlowdimlem13  25141  axlowdimlem16  25144  axcontlem4  25154  axcontlem10  25160  bpolycl  25346  bpolysum  25347  bpolydiflem  25348  supaddc  25482  supadd  25483  itg2addnclem2  25493  ftc1cnnclem  25513  ftc1cnnc  25514  areacirclem4  25519  areacirclem5  25521  areacirc  25523  opnrebl2  25560  fnessex  25599  fneuni  25600  comppfsc  25631  neibastop1  25632  neibastop2lem  25633  neibastop3  25635  sdclem1  25777  mettrifi  25797  sstotbnd2  25821  equivtotbnd  25825  isbndx  25829  totbndbnd  25836  equivbnd2  25839  cntotbnd  25843  heibor1lem  25856  heiborlem3  25860  heibor  25868  iccbnd  25887  idlcl  25965  divrngidl  25976  ismrcd1  26096  mzpf  26137  mzpindd  26147  fphpdo  26223  pell14qrre  26265  pell14qrne0  26266  elpell14qr2  26270  elpell1qr2  26280  pellfundex  26294  dnnumch3lem  26466  dnnumch3  26467  fnwe2lem2  26471  aomclem4  26477  kelac1  26484  kercvrlsm  26504  dsmmsubg  26532  frlmsslsp  26571  hbtlem2  26651  hbtlem5  26655  flcidc  26702  f1omvdmvd  26709  f1omvdconj  26712  symggen  26734  psgnunilem5  26740  psgnunilem2  26741  cntzsdrg  26833  climinf  27055  stoweidlem18  27090  stoweidlem26  27098  stoweidlem27  27099  stoweidlem31  27103  stoweidlem35  27107  stoweidlem39  27111  stoweidlem42  27114  stoweidlem48  27120  stoweidlem51  27123  stoweidlem56  27128  stoweidlem61  27133  redwlk  27742  bnj1137  28787  bnj1498  28853  lsatfixedN  29268  elpaddn0  30058  diaintclN  31317  dibglbN  31425  dibintclN  31426  dihrnlss  31536  dihglblem3N  31554  dihglblem6  31599  dihintcl  31603  dochkr1  31737  dochkr1OLDN  31738  lcfrlem5  31805  lcfr  31844  mapdrvallem2  31904  hgmapvvlem3  32187  hdmapoc  32193  hlhilocv  32219
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-in 3235  df-ss 3242
  Copyright terms: Public domain W3C validator