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

Theorem sselda 3504
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 3503 . 2  |-  ( ph  ->  ( C  e.  A  ->  C  e.  B ) )
32imp 429 1  |-  ( (
ph  /\  C  e.  A )  ->  C  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1767    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  elrel  5103  ffvresb  6050  1stdm  6828  tfrlem1  7042  oeeulem  7247  swoso  7339  erinxp  7382  boxcutc  7509  fundmen  7586  suplub2  7917  supisolem  7927  ordiso2  7936  ordtypelem2  7940  ordtypelem6  7944  ordtypelem7  7945  cantnflt  8087  cantnflem1c  8102  cantnflem1d  8103  cantnflem1  8104  cantnflem3  8106  cantnf  8108  cantnfltOLD  8117  cantnflem1cOLD  8125  cantnflem1dOLD  8126  cantnflem1OLD  8127  cantnflem3OLD  8128  cantnfOLD  8130  cnfcomlem  8139  cnfcom3lem  8143  cnfcomlemOLD  8147  cnfcom3lemOLD  8151  rankelb  8238  rankval3b  8240  ackbij2lem1  8595  ackbij1lem9  8604  ackbij1lem10  8605  ackbij1lem18  8613  ackbij2lem3  8617  ackbij2  8619  fin23lem7  8692  enfin2i  8697  isf32lem9  8737  isf34lem4  8753  fin1a2lem11  8786  hsmexlem4  8805  ttukeylem6  8890  fpwwe2lem8  9011  fpwwe2lem9  9012  fpwwe2  9017  canth4  9021  intwun  9109  wuncval2  9121  inttsk  9148  rankcf  9151  r1tskina  9156  tskuni  9157  elprnq  9365  dedekind  9739  suprub  10500  suprleub  10503  supmul1  10504  supmullem1  10505  supmul  10507  infmrgelb  10519  un0addcl  10825  un0mulcl  10826  suprzcl  10936  zsupss  11167  supxrleub  11514  supxrre  11515  supxrss  11520  infmxrgelb  11522  infmxrre  11523  icoshftf1o  11639  supicc  11664  supiccub  11665  supicclub  11666  supicclub2  11667  elfzom1elfzo  11848  zpnn0elfzo  11852  uzindi  12054  seqcl  12090  seqfveq  12094  monoord2  12101  sermono  12102  seqsplit  12103  seqcaopr2  12106  seqf1olem2a  12108  seqf1olem2  12110  seqhomo  12117  seqz  12118  seqof2  12128  seqcoll  12472  seqcoll2  12473  ccatval1  12554  ccatass  12564  revccat  12697  rexanre  13135  rexuzre  13141  rexico  13142  limsupgle  13256  limsupval2  13259  limsupgre  13260  limsupbnd2  13262  rlim2lt  13276  rlim3  13277  ello12  13295  lo1bdd2  13303  elo12  13306  rlimclim1  13324  climrlim2  13326  lo1resb  13343  o1resb  13345  rlimcn2  13369  o1of2  13391  rlimsqzlem  13427  isercolllem3  13445  isercoll2  13447  climsup  13448  iseraltlem2  13461  summolem2a  13493  sumss  13502  fsumss  13503  fsumcvg3  13507  fsumsplit  13518  fsum2dlem  13541  fsum0diag2  13554  fsumless  13566  fsumabs  13571  telfsumo  13572  fsumparts  13576  fsumrlim  13581  fsumo1  13582  o1fsum  13583  fsumiun  13591  hashuni  13594  ackbijnn  13596  binom1dif  13601  incexclem  13604  isumsplit  13608  isumrpcl  13611  isumless  13613  isumltss  13616  supcvg  13623  cvgrat  13648  mertenslem1  13649  rpnnen2  13813  bitsinv2  13945  bitsf1ocnv  13946  bitsinvp1  13951  eulerthlem2  14164  4sqlem11  14325  vdwlem6  14356  ramval  14378  ramcl2lem  14379  restid2  14679  mress  14841  mremre  14852  mreacs  14906  fullsubc  15070  subsubc  15073  funcres  15116  fuciso  15195  setcmon  15265  setcepi  15266  catccatid  15280  drsdirfi  15418  clatglbss  15607  ipodrsfi  15643  isacs3lem  15646  mrelatglb  15664  mrelatlub  15666  issubmnd  15759  ress0g  15760  gsumress  15817  gsumwspan  15834  frmdsssubm  15849  frmdss2  15851  grpinvssd  15913  subginv  16000  issubg2  16008  issubg4  16012  ssnmz  16035  lagsubg2  16054  resghm  16075  conjnmz  16092  conjnmzb  16093  subgga  16130  gass  16131  gasubg  16132  cntzsubm  16165  cntzmhm  16168  f1omvdmvd  16261  f1omvdconj  16264  symggen  16288  psgnunilem5  16312  psgnunilem2  16313  submod  16382  sylow1lem2  16412  sylow1lem3  16413  sylow1lem4  16414  sylow2alem2  16431  sylow2a  16432  sylow2blem2  16434  sylow3lem1  16440  sylow3lem6  16445  lsmssv  16456  lsmub2x  16460  lsmelvalm  16464  lsmcom2  16468  pj1lid  16512  pj1rid  16513  efgrelexlemb  16561  frgpup1  16586  frgpup3lem  16588  cntzcmn  16638  gsumval3eu  16695  gsumval3OLD  16696  gsumval3  16699  gsumzaddlem  16722  gsumzaddlemOLD  16724  gsumzoppg  16755  gsumzoppgOLD  16756  dprdfadd  16847  dprdfaddOLD  16854  dprdres  16862  dprdcntz2  16873  dprddisj2  16874  dprddisj2OLD  16875  dprd2dlem1  16877  dmdprdsplit2lem  16881  ablfac1lem  16906  ablfac1b  16908  ablfac1c  16909  ablfac1eu  16911  pgpfac1lem1  16912  pgpfac1lem2  16913  pgpfac1lem3  16915  pgpfac1lem4  16916  ablfaclem3  16925  rngidss  17009  invrpropd  17128  subrg1  17219  subrginv  17225  subrgunit  17227  cntzsubr  17241  abvres  17268  lssel  17364  islss3  17385  lssintcl  17390  lmhmima  17473  lmhmpreima  17474  lbsel  17504  lbspropd  17525  lsmcv  17567  lspsolvlem  17568  lbsextlem2  17585  lidlsubcl  17643  drngnidl  17656  issubassa2  17762  mplcoe1  17895  mplcoe5lem  17898  mplcoe5  17899  mplcoe2OLD  17901  subrgascl  17931  subrgasclcl  17932  zringlpirlem1  18273  zlpirlem1  18278  regsumsupp  18422  ocvocv  18466  ocvlss  18467  pjfo  18510  ocvpj  18512  obsne0  18520  obselocv  18523  dsmmsubg  18538  frlmsslsp  18593  frlmsslspOLD  18594  ofco2  18717  mdetrsca2  18870  mdetunilem9  18886  madugsum  18909  tgclb  19235  tgidm  19245  pptbas  19272  toponmre  19357  neiptoptop  19395  neiptopnei  19396  neiptopreu  19397  clslp  19412  tgrest  19423  perfopn  19449  ordtbas  19456  ordtrest2lem  19467  pnrmcld  19606  ist1-3  19613  isreg2  19641  cncmp  19655  cmpsublem  19662  tgcmp  19664  cmpcld  19665  hauscmplem  19669  2ndcomap  19722  1stcelcls  19725  restlly  19747  lly1stc  19760  kgentopon  19771  llycmpkgen2  19783  txcls  19837  ptclsg  19848  txcnp  19853  txdis1cn  19868  txcmplem1  19874  txkgen  19885  xkoptsub  19887  xkopt  19888  xkococnlem  19892  xkoinjcn  19920  basqtop  19944  tgqtop  19945  kqfvima  19963  kqreglem1  19974  fbelss  20066  fbssfi  20070  fgabs  20112  trfg  20124  uffixfr  20156  uffixsn  20158  elfm2  20181  fmfnfmlem4  20190  fmfnfm  20191  flimnei  20200  flimrest  20216  flimcls  20218  flimsncls  20219  flffbas  20228  fclsrest  20257  fclscmp  20263  alexsublem  20276  ptcmplem3  20286  ptcmplem4  20287  cnextfres  20300  subgntr  20337  opnsubg  20338  clssubg  20339  tgpconcomp  20343  divstgpopn  20350  divstgplem  20351  tsmssubm  20376  tgptsmscls  20384  tgptsmscld  20385  tsmsxplem1  20387  tsmsxplem2  20388  ustssxp  20439  ustuqtop4  20479  utopsnneiplem  20482  utop2nei  20485  isucn2  20514  ucnima  20516  psmetres2  20550  imasdsf1olem  20608  blpnfctr  20671  xmetresbl  20672  mopni2  20728  mopni3  20729  rnblopn  20734  metustexhalfOLD  20798  metustexhalf  20799  metutopOLD  20817  psmetutop  20818  tgioo  21033  xrsmopn  21049  zdis  21053  icccmplem3  21061  reconnlem2  21064  opnreen  21068  metdsf  21084  metdsge  21085  metdsle  21088  metdsre  21089  metnrmlem2  21096  metnrmlem3  21097  fsumcn  21106  climcncf  21136  icccvx  21182  cnheibor  21187  bndth  21190  lebnumlem1  21193  lebnumlem2  21194  pi1grplem  21281  clmneg  21313  nmoleub2lem3  21330  cphsqrtcl  21363  cphabscl  21364  clsocv  21422  iscfil2  21437  cfil3i  21440  cfilfcls  21445  cmetcaulem  21459  iscmet3lem2  21463  cfilresi  21466  caussi  21468  lmclim  21473  rrxnm  21555  rrxcph  21556  rrxmval  21564  rrxmetlem  21566  rrxmet  21567  rrxdstprj1  21568  minveclem1  21571  minveclem3b  21575  minveclem4  21579  minveclem6  21581  pjthlem2  21585  ivth2  21599  ivthicc  21602  ovollb2lem  21631  ovoliunlem1  21645  ovolicc2lem4  21663  ioombl1lem4  21703  dyadmax  21739  dyadmbl  21741  opnmbllem  21742  volsup2  21746  volivth  21748  vitalilem5  21753  i1fima  21817  i1fd  21820  itg1val2  21823  itg1cl  21824  itg1ge0  21825  itg11  21830  i1fadd  21834  i1fmul  21835  itg1addlem4  21838  itg1addlem5  21839  i1fmulc  21842  itg1mulc  21843  itg10a  21849  itg1ge0a  21850  itg1climres  21853  mbfi1fseqlem4  21857  mbfi1fseqlem5  21858  mbfi1flim  21862  mbfmullem2  21863  itg2const2  21880  itg2splitlem  21887  itg2split  21888  itg2gt0  21899  itg2cnlem2  21901  iblss  21943  iblss2  21944  itgss3  21953  itgless  21955  itgfsum  21965  itgsplit  21974  itgsplitioo  21976  itggt0  21980  itgcn  21981  ditgcl  21994  ditgswap  21995  ditgsplitlem  21996  ellimc3  22015  perfdvf  22039  dvreslem  22045  dvcnp  22054  dvcnp2  22055  dvaddbr  22073  dvmulbr  22074  dvcjbr  22084  dvmptfsum  22108  dvcnvlem  22109  dvlip  22126  dvlipcn  22127  dvlip2  22128  dv11cn  22134  dvivthlem1  22141  dvivthlem2  22142  dvne0  22144  lhop1lem  22146  lhop2  22148  lhop  22149  dvcvx  22153  dvfsumle  22154  dvfsumge  22155  dvfsumabs  22156  dvfsumlem2  22160  dvfsumlem3  22161  dvfsumrlimge0  22163  dvfsumrlim2  22165  ftc1lem1  22168  ftc1lem4  22172  ftc1lem6  22174  itgsubstlem  22181  ig1peu  22304  plyeq0lem  22339  plypf1  22341  coeeulem  22353  vieta1lem1  22437  vieta1lem2  22438  plyexmo  22440  taylthlem1  22499  taylthlem2  22500  ulmdvlem1  22526  ulmdvlem3  22528  mtest  22530  radcnv0  22542  pserulm  22548  psercnlem2  22550  psercnlem1  22551  psercn  22552  pserdvlem1  22553  pserdvlem2  22554  pserdv  22555  pserdv2  22556  abelthlem3  22559  abelthlem4  22560  abelthlem9  22566  pige3  22640  efif1olem4  22662  efopnlem2  22763  efopn  22764  logccv  22769  loglesqrt  22857  rlimcnp  23020  rlimcnp2  23021  xrlimcnp  23023  efrlim  23024  jensenlem1  23041  jensenlem2  23042  jensen  23043  fsumharmonic  23066  wilthlem2  23068  basellem3  23081  basellem5  23083  chtdif  23157  sqff1o  23181  musumsum  23193  muinv  23194  chtublem  23211  fsumvma  23213  vmasum  23216  chpval2  23218  chpchtsum  23219  chpub  23220  perfectlem2  23230  lgsquadlem2  23355  chebbnd1lem1  23379  dchrisumlem2  23400  dchrisumlem3  23401  dchrmusum2  23404  dchrisum0fno1  23421  rpvmasum2  23422  dchrisum0lem1b  23425  dchrisum0lem1  23426  rplogsum  23437  mudivsum  23440  mulogsum  23442  mulog2sumlem2  23445  selberg2lem  23460  chpdifbndlem1  23463  pntrlog2bndlem6  23493  pntrlog2bnd  23494  pntlemj  23513  pntlemf  23515  pntlem3  23519  tglineelsb2  23723  tglinecom  23726  axlowdimlem13  23930  axlowdimlem16  23933  axcontlem4  23943  axcontlem10  23949  umgraex  23996  edg  24026  redwlk  24281  wwlkm1edg  24408  clwlkisclwwlklem2fv1  24455  clwlkisclwwlklem1  24460  clwwlkvbij  24474  clwwisshclwwlem  24479  clwlkfclwwlk  24517  eupares  24648  subgoinv  24983  ubthlem1  25459  ubthlem2  25460  ubthlem3  25461  minvecolem1  25463  minvecolem4  25469  minvecolem5  25470  minvecolem6  25471  shel  25801  chel  25821  ocorth  25882  pjpreeq  25989  chscllem1  26228  chscllem2  26229  spansncvi  26243  off2  27151  xppreima  27156  ofpreima  27176  ofpreima2  27177  fcnvgreu  27183  supxrnemnf  27248  ssnnssfz  27262  iundisjfi  27266  hashunif  27270  toslublem  27314  tosglblem  27316  gsumvsca1  27433  gsumvsca2  27434  ress1r  27439  tpr2rico  27527  ordtrest2NEWlem  27537  ordtconlem1  27539  fsumcvg4  27565  indsum  27673  esummono  27703  gsumesum  27704  elsigass  27762  elsigagen  27784  measiuns  27825  measres  27830  volmeas  27840  sibfof  27919  sitgclg  27921  eulerpartlemsv2  27934  eulerpartlemsf  27935  eulerpartlemsv3  27937  eulerpartlemgc  27938  eulerpartlemv  27940  eulerpartlemb  27944  eulerpartlemf  27946  eulerpartlemr  27950  eulerpartlemgvv  27952  eulerpartlemgu  27953  eulerpartlemgs2  27956  ballotlemsel1i  28088  ballotlemsima  28091  ballotlemfrceq  28104  signsplypnf  28144  signsply0  28145  signstcl  28159  signstf  28160  signstfvn  28163  signstfvp  28165  signsvfn  28176  lgamgulmlem2  28209  lgamgulm2  28215  lgambdd  28216  erdszelem8  28279  cvmscld  28355  cvmsss2  28356  cvmopnlem  28360  cvmlift2lem9  28393  cvmlift2lem11  28395  cvmlift2lem12  28396  cvmliftpht  28400  clim2prod  28596  prodfn0  28602  prodfrec  28603  prodmolem2a  28640  fprodntriv  28648  prodss  28653  fprodss  28654  fprodsplit  28669  fprod2dlem  28684  binomfallfaclem2  28736  trpredelss  28889  sltres  28998  nobndup  29034  nobnddown  29035  nofulllem5  29040  bpolycl  29388  bpolysum  29389  bpolydiflem  29390  supaddc  29615  supadd  29616  opnmbllem0  29625  mblfinlem2  29627  ismblfin  29630  cnambfre  29638  itg2addnclem2  29642  ftc1cnnclem  29663  ftc1cnnc  29664  ftc1anclem6  29670  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  ftc2nc  29674  areacirclem2  29683  areacirclem4  29685  areacirc  29687  opnrebl2  29714  fnessex  29745  fneuni  29746  comppfsc  29777  neibastop1  29778  neibastop2lem  29779  neibastop3  29781  sdclem1  29837  mettrifi  29851  sstotbnd2  29871  equivtotbnd  29875  isbndx  29879  totbndbnd  29886  equivbnd2  29889  cntotbnd  29893  heibor1lem  29906  heiborlem3  29910  heibor  29918  iccbnd  29937  idlcl  30015  divrngidl  30026  ismrcd1  30232  mzpf  30270  mzpindd  30280  fphpdo  30353  pell14qrre  30395  pell14qrne0  30396  elpell14qr2  30400  elpell1qr2  30410  pellfundex  30424  dnnumch3lem  30596  dnnumch3  30597  fnwe2lem2  30601  aomclem4  30607  kelac1  30613  kercvrlsm  30633  hbtlem2  30677  hbtlem5  30681  flcidc  30728  cntzsdrg  30756  itgpowd  30787  areaquad  30789  infmxrss  31069  ssfiunibd  31086  iccshift  31122  iooshift  31126  fmul01  31130  fmulcl  31131  climinf  31148  mullimc  31158  mullimcf  31165  idlimc  31168  limcperiod  31170  limcrecl  31171  limcresiooub  31184  limcresioolb  31185  limcleqr  31186  addlimc  31190  limclner  31193  cncfmptssg  31208  cncfshift  31212  cncfperiod  31217  icccncfext  31226  dvbdfbdioolem1  31258  ibliccsinexp  31268  iblioosinexp  31270  itgcoscmulx  31287  itgioocnicc  31295  itgiccshift  31298  itgperiod  31299  itgsbtaddcnst  31300  stoweidlem5  31305  stoweidlem11  31311  stoweidlem17  31317  stoweidlem18  31318  stoweidlem26  31326  stoweidlem27  31327  stoweidlem31  31331  stoweidlem35  31335  stoweidlem39  31339  stoweidlem42  31342  stoweidlem43  31343  stoweidlem44  31344  stoweidlem48  31348  stoweidlem51  31351  stoweidlem52  31352  stoweidlem56  31356  stoweidlem57  31357  stoweidlem59  31359  stoweidlem60  31360  stoweidlem61  31361  dirkeritg  31402  dirkercncflem2  31404  dirkercncflem4  31406  fourierdlem18  31425  fourierdlem39  31446  fourierdlem42  31449  fourierdlem48  31455  fourierdlem49  31456  fourierdlem51  31458  fourierdlem53  31460  fourierdlem57  31464  fourierdlem64  31471  fourierdlem72  31479  fourierdlem74  31481  fourierdlem75  31482  fourierdlem76  31483  fourierdlem79  31486  fourierdlem80  31487  fourierdlem81  31488  fourierdlem83  31490  fourierdlem90  31497  fourierdlem93  31500  fourierdlem95  31502  fourierdlem97  31504  fourierdlem101  31508  fourierdlem103  31510  fourierdlem104  31511  fourierdlem111  31518  fourierdlem112  31519  fourierdlem113  31520  fouriersw  31532  elpwdifsn  31763  ssnn0ssfz  32002  lincresunit3  32155  bnj1137  33130  bnj1498  33196  lsatfixedN  33806  elpaddn0  34596  diaintclN  35855  dibglbN  35963  dibintclN  35964  dihrnlss  36074  dihglblem3N  36092  dihglblem6  36137  dihintcl  36141  dochkr1  36275  dochkr1OLDN  36276  lcfrlem5  36343  lcfr  36382  mapdrvallem2  36442  hgmapvvlem3  36725  hdmapoc  36731  hlhilocv  36757
  Copyright terms: Public domain W3C validator