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

Theorem sselda 3340
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 3339 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 419 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725    C_ wss 3312
This theorem is referenced by:  elrel  4969  ffvresb  5891  1stdm  6385  oeeulem  6835  swoso  6927  erinxp  6969  boxcutc  7096  fundmen  7171  suplub2  7455  supisolem  7464  ordiso2  7473  ordtypelem2  7477  ordtypelem6  7481  ordtypelem7  7482  cantnflt  7616  cantnflem1c  7632  cantnflem1d  7633  cantnflem1  7634  cantnflem3  7636  cantnf  7638  cnfcomlem  7645  cnfcom3lem  7649  rankelb  7739  rankval3b  7741  ackbij2lem1  8088  ackbij1lem9  8097  ackbij1lem10  8098  ackbij1lem18  8106  ackbij2lem3  8110  ackbij2  8112  fin23lem7  8185  enfin2i  8190  isf32lem9  8230  isf34lem4  8246  fin1a2lem11  8279  hsmexlem4  8298  ttukeylem6  8383  fpwwe2lem8  8501  fpwwe2lem9  8502  fpwwe2  8507  canth4  8511  intwun  8599  wuncval2  8611  inttsk  8638  rankcf  8641  r1tskina  8646  tskuni  8647  elprnq  8857  suprub  9958  suprleub  9961  supmul1  9962  supmullem1  9963  supmul  9965  infmrgelb  9977  un0addcl  10242  un0mulcl  10243  suprzcl  10338  zsupss  10554  supxrleub  10894  supxrre  10895  supxrss  10900  infmxrgelb  10902  infmxrre  10903  icoshftf1o  11009  uzindi  11308  seqcl  11331  seqfveq  11335  monoord2  11342  sermono  11343  seqsplit  11344  seqcaopr2  11347  seqf1olem2a  11349  seqf1olem2  11351  seqhomo  11358  seqz  11359  seqof2  11369  seqcoll  11700  seqcoll2  11701  ccatval1  11733  ccatass  11738  revccat  11786  rexanre  12138  rexuzre  12144  rexico  12145  limsupgle  12259  limsupval2  12262  limsupgre  12263  limsupbnd2  12265  rlim2lt  12279  rlim3  12280  ello12  12298  lo1bdd2  12306  elo12  12309  rlimclim1  12327  climrlim2  12329  lo1resb  12346  o1resb  12348  rlimcn2  12372  o1of2  12394  rlimsqzlem  12430  isercolllem3  12448  isercoll2  12450  climsup  12451  iseraltlem2  12464  summolem2a  12497  sumss  12506  fsumss  12507  fsumcvg3  12511  fsumsplit  12521  fsum2dlem  12542  fsum0diag2  12554  fsumless  12563  fsumabs  12568  fsumtscopo  12569  fsumparts  12573  fsumrlim  12578  fsumo1  12579  o1fsum  12580  fsumiun  12588  hashuni  12592  hashuniOLD  12593  ackbijnn  12595  binom1dif  12600  incexclem  12604  isumsplit  12608  isumrpcl  12611  isumless  12613  isumltss  12616  supcvg  12623  cvgrat  12648  mertenslem1  12649  rpnnen2  12813  bitsinv2  12943  bitsf1ocnv  12944  bitsinvp1  12949  eulerthlem2  13159  4sqlem11  13311  vdwlem6  13342  ramval  13364  ramcl2lem  13365  restid2  13646  mress  13806  mremre  13817  mreacs  13871  fullsubc  14035  subsubc  14038  funcres  14081  fuciso  14160  setcmon  14230  setcepi  14231  catccatid  14245  drsdirfi  14383  clatglbss  14542  ipodrsfi  14577  isacs3lem  14580  mrelatglb  14598  mrelatlub  14600  issubmnd  14712  gsumress  14765  gsumwspan  14779  frmdsssubm  14794  frmdss2  14796  subginv  14939  issubg2  14947  issubg4  14949  ssnmz  14970  lagsubg2  14989  resghm  15010  conjnmz  15027  conjnmzb  15028  subgga  15065  gass  15066  gasubg  15067  cntzsubm  15122  cntzmhm  15125  submod  15191  sylow1lem2  15221  sylow1lem3  15222  sylow1lem4  15223  sylow2alem2  15240  sylow2a  15241  sylow2blem2  15243  sylow3lem1  15249  sylow3lem6  15254  lsmssv  15265  lsmub2x  15269  lsmelvalm  15273  lsmcom2  15277  pj1lid  15321  pj1rid  15322  efgrelexlemb  15370  frgpup1  15395  frgpup3lem  15397  cntzcmn  15447  gsumval3eu  15501  gsumval3  15502  gsumzaddlem  15514  gsumzoppg  15527  dprdfadd  15566  dprdres  15574  dprdcntz2  15584  dprddisj2  15585  dprd2dlem1  15587  dmdprdsplit2lem  15591  ablfac1lem  15614  ablfac1b  15616  ablfac1c  15617  ablfac1eu  15619  pgpfac1lem1  15620  pgpfac1lem2  15621  pgpfac1lem3  15623  pgpfac1lem4  15624  ablfaclem3  15633  rngidss  15678  invrpropd  15791  subrg1  15866  subrginv  15872  subrgunit  15874  cntzsubr  15888  abvres  15915  lssel  16002  islss3  16023  lssintcl  16028  lmhmima  16111  lmhmpreima  16112  lbsel  16138  lbspropd  16159  lsmcv  16201  lspsolvlem  16202  lbsextlem2  16219  lidlsubcl  16275  drngnidl  16288  issubassa2  16391  mplcoe1  16516  mplcoe2  16518  subrgascl  16546  subrgasclcl  16547  zlpirlem1  16756  ocvocv  16886  ocvlss  16887  pjfo  16930  ocvpj  16932  obsne0  16940  obselocv  16943  tgclb  17023  tgidm  17033  pptbas  17060  toponmre  17145  neiptoptop  17183  neiptopnei  17184  neiptopreu  17185  clslp  17200  tgrest  17211  perfopn  17237  ordtbas  17244  ordtrest2lem  17255  pnrmcld  17394  ist1-3  17401  isreg2  17429  cncmp  17443  cmpsublem  17450  tgcmp  17452  cmpcld  17453  hauscmplem  17457  2ndcomap  17509  1stcelcls  17512  restlly  17534  lly1stc  17547  kgentopon  17558  llycmpkgen2  17570  txcls  17624  ptclsg  17635  txcnp  17640  txdis1cn  17655  txcmplem1  17661  txkgen  17672  xkoptsub  17674  xkopt  17675  xkococnlem  17679  xkoinjcn  17707  basqtop  17731  tgqtop  17732  kqfvima  17750  kqreglem1  17761  fbelss  17853  fbssfi  17857  fgabs  17899  trfg  17911  uffixfr  17943  uffixsn  17945  elfm2  17968  fmfnfmlem4  17977  fmfnfm  17978  flimnei  17987  flimrest  18003  flimcls  18005  flimsncls  18006  flffbas  18015  fclsrest  18044  fclscmp  18050  alexsublem  18063  ptcmplem3  18073  ptcmplem4  18074  cnextfres  18087  subgntr  18124  opnsubg  18125  clssubg  18126  tgpconcomp  18130  divstgpopn  18137  divstgplem  18138  tsmssubm  18160  tgptsmscls  18167  tgptsmscld  18168  tsmsxplem1  18170  tsmsxplem2  18171  ustssxp  18222  ustuqtop4  18262  utopsnneiplem  18265  utop2nei  18268  isucn2  18297  ucnima  18299  psmetres2  18333  imasdsf1olem  18391  blpnfctr  18454  xmetresbl  18455  mopni2  18511  mopni3  18512  rnblopn  18517  metustexhalfOLD  18581  metustexhalf  18582  metutopOLD  18600  psmetutop  18601  tgioo  18815  xrsmopn  18831  zdis  18835  icccmplem3  18843  reconnlem2  18846  opnreen  18850  metdsf  18866  metdsge  18867  metdsle  18870  metdsre  18871  metnrmlem2  18878  metnrmlem3  18879  fsumcn  18888  climcncf  18918  icccvx  18963  cnheibor  18968  bndth  18971  lebnumlem1  18974  lebnumlem2  18975  pi1grplem  19062  clmneg  19094  nmoleub2lem3  19111  cphsqrcl  19135  cphabscl  19136  clsocv  19192  iscfil2  19207  cfil3i  19210  cfilfcls  19215  cmetcaulem  19229  iscmet3lem2  19233  cfilresi  19236  caussi  19238  lmclim  19243  minveclem1  19313  minveclem3b  19317  minveclem4  19321  minveclem6  19323  pjthlem2  19327  ivth2  19340  ivthicc  19343  ovollb2lem  19372  ovoliunlem1  19386  ovolicc2lem4  19404  ioombl1lem4  19443  dyadmax  19478  dyadmbl  19480  opnmbllem  19481  volsup2  19485  volivth  19487  vitalilem5  19492  i1fima  19558  i1fd  19561  itg1val2  19564  itg1cl  19565  itg1ge0  19566  itg11  19571  i1fadd  19575  i1fmul  19576  itg1addlem4  19579  itg1addlem5  19580  i1fmulc  19583  itg1mulc  19584  itg10a  19590  itg1ge0a  19591  itg1climres  19594  mbfi1fseqlem4  19598  mbfi1fseqlem5  19599  mbfi1flim  19603  mbfmullem2  19604  itg2const2  19621  itg2splitlem  19628  itg2split  19629  itg2gt0  19640  itg2cnlem2  19642  iblss  19684  iblss2  19685  itgss3  19694  itgless  19696  itgfsum  19706  itgsplit  19715  itgsplitioo  19717  itggt0  19721  itgcn  19722  ditgcl  19733  ditgswap  19734  ditgsplitlem  19735  ellimc3  19754  perfdvf  19778  dvreslem  19784  dvcnp  19793  dvcnp2  19794  dvaddbr  19812  dvmulbr  19813  dvcjbr  19823  dvmptfsum  19847  dvcnvlem  19848  dvlip  19865  dvlipcn  19866  dvlip2  19867  dv11cn  19873  dvivthlem1  19880  dvivthlem2  19881  dvne0  19883  lhop1lem  19885  lhop2  19887  lhop  19888  dvcvx  19892  dvfsumle  19893  dvfsumge  19894  dvfsumabs  19895  dvfsumlem2  19899  dvfsumlem3  19900  dvfsumrlimge0  19902  dvfsumrlim2  19904  ftc1lem1  19907  ftc1lem4  19911  ftc1lem6  19913  itgsubstlem  19920  ig1peu  20082  plyeq0lem  20117  plypf1  20119  coeeulem  20131  vieta1lem1  20215  vieta1lem2  20216  plyexmo  20218  aaliou3lem2  20248  taylthlem1  20277  taylthlem2  20278  ulmdvlem1  20304  ulmdvlem3  20306  mtest  20308  radcnv0  20320  pserulm  20326  psercnlem2  20328  psercnlem1  20329  psercn  20330  pserdvlem1  20331  pserdvlem2  20332  pserdv  20333  pserdv2  20334  abelthlem3  20337  abelthlem4  20338  abelthlem9  20344  pige3  20413  efif1olem4  20435  efopnlem2  20536  efopn  20537  logccv  20542  loglesqr  20630  rlimcnp  20792  rlimcnp2  20793  xrlimcnp  20795  efrlim  20796  jensenlem1  20813  jensenlem2  20814  jensen  20815  fsumharmonic  20838  wilthlem2  20840  basellem3  20853  basellem5  20855  chtdif  20929  sqff1o  20953  musumsum  20965  muinv  20966  chtublem  20983  fsumvma  20985  vmasum  20988  chpval2  20990  chpchtsum  20991  chpub  20992  perfectlem2  21002  lgsquadlem2  21127  chebbnd1lem1  21151  dchrisumlem2  21172  dchrisumlem3  21173  dchrmusum2  21176  dchrisum0fno1  21193  rpvmasum2  21194  dchrisum0lem1b  21197  dchrisum0lem1  21198  rplogsum  21209  mudivsum  21212  mulogsum  21214  mulog2sumlem2  21217  selberg2lem  21232  chpdifbndlem1  21235  pntrlog2bndlem6  21265  pntrlog2bnd  21266  pntlemj  21285  pntlemf  21287  pntlem3  21291  umgraex  21346  redwlk  21594  eupares  21685  subgoinv  21884  ubthlem1  22360  ubthlem2  22361  ubthlem3  22362  minvecolem1  22364  minvecolem4  22370  minvecolem5  22371  minvecolem6  22372  shel  22701  chel  22721  ocorth  22781  pjpreeq  22888  chscllem1  23127  chscllem2  23128  spansncvi  23142  off2  24042  xppreima  24047  ofpreima  24069  supxrnemnf  24115  ssnnssfz  24136  iundisjfi  24140  hashunif  24146  ress0g  24170  toslub  24179  tosglb  24180  tpr2rico  24298  indsum  24408  esummono  24438  gsumesum  24439  elsigass  24496  elsigagen  24518  measiuns  24559  measres  24564  volmeas  24575  sibfof  24642  sitgclg  24644  ballotlemsel1i  24758  ballotlemsima  24761  ballotlemfrceq  24774  lgamgulmlem2  24802  lgamgulm2  24808  lgambdd  24809  erdszelem8  24872  cvmscld  24948  cvmsss2  24949  cvmopnlem  24953  cvmlift2lem9  24986  cvmlift2lem11  24988  cvmlift2lem12  24989  cvmliftpht  24993  dedekind  25175  clim2prod  25205  prodfn0  25211  prodfrec  25212  prodmolem2a  25249  fprodntriv  25257  prodss  25262  fprodss  25263  fprodsplit  25278  fprod2dlem  25293  binomfallfaclem2  25345  trpredelss  25490  sltres  25573  nobndup  25609  nobnddown  25610  nofulllem5  25615  axlowdimlem13  25841  axlowdimlem16  25844  axcontlem4  25854  axcontlem10  25860  bpolycl  26046  bpolysum  26047  bpolydiflem  26048  supaddc  26184  supadd  26185  mblfinlem  26190  ismblfin  26193  cnambfre  26201  itg2addnclem2  26203  ftc1cnnclem  26224  ftc1cnnc  26225  areacirclem4  26230  areacirclem5  26232  areacirc  26234  opnrebl2  26261  fnessex  26292  fneuni  26293  comppfsc  26324  neibastop1  26325  neibastop2lem  26326  neibastop3  26328  sdclem1  26384  mettrifi  26400  sstotbnd2  26420  equivtotbnd  26424  isbndx  26428  totbndbnd  26435  equivbnd2  26438  cntotbnd  26442  heibor1lem  26455  heiborlem3  26459  heibor  26467  iccbnd  26486  idlcl  26564  divrngidl  26575  ismrcd1  26689  mzpf  26730  mzpindd  26740  fphpdo  26815  pell14qrre  26857  pell14qrne0  26858  elpell14qr2  26862  elpell1qr2  26872  pellfundex  26886  dnnumch3lem  27058  dnnumch3  27059  fnwe2lem2  27063  aomclem4  27069  kelac1  27076  kercvrlsm  27096  dsmmsubg  27124  frlmsslsp  27163  hbtlem2  27243  hbtlem5  27247  flcidc  27294  f1omvdmvd  27301  f1omvdconj  27304  symggen  27326  psgnunilem5  27332  psgnunilem2  27333  cntzsdrg  27425  fmul01  27624  fmulcl  27625  climinf  27646  ibliccsinexp  27659  iblioosinexp  27661  stoweidlem5  27668  stoweidlem7  27670  stoweidlem11  27674  stoweidlem17  27680  stoweidlem18  27681  stoweidlem26  27689  stoweidlem27  27690  stoweidlem31  27694  stoweidlem35  27698  stoweidlem39  27702  stoweidlem42  27705  stoweidlem43  27706  stoweidlem44  27707  stoweidlem48  27711  stoweidlem51  27714  stoweidlem52  27715  stoweidlem56  27719  stoweidlem57  27720  stoweidlem59  27722  stoweidlem60  27723  stoweidlem61  27724  swrd0swrd  28084  swrdccatin2lem1  28092  swrdccatin2  28093  swrdccatin12  28101  bnj1137  29218  bnj1498  29284  lsatfixedN  29646  elpaddn0  30436  diaintclN  31695  dibglbN  31803  dibintclN  31804  dihrnlss  31914  dihglblem3N  31932  dihglblem6  31977  dihintcl  31981  dochkr1  32115  dochkr1OLDN  32116  lcfrlem5  32183  lcfr  32222  mapdrvallem2  32282  hgmapvvlem3  32565  hdmapoc  32571  hlhilocv  32597
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326
  Copyright terms: Public domain W3C validator