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

Theorem sselda 3344
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 3343 . 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 1755    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  elrel  4929  ffvresb  5861  1stdm  6610  tfrlem1  6821  oeeulem  7028  swoso  7120  erinxp  7162  boxcutc  7294  fundmen  7371  suplub2  7699  supisolem  7708  ordiso2  7717  ordtypelem2  7721  ordtypelem6  7725  ordtypelem7  7726  cantnflt  7868  cantnflem1c  7883  cantnflem1d  7884  cantnflem1  7885  cantnflem3  7887  cantnf  7889  cantnfltOLD  7898  cantnflem1cOLD  7906  cantnflem1dOLD  7907  cantnflem1OLD  7908  cantnflem3OLD  7909  cantnfOLD  7911  cnfcomlem  7920  cnfcom3lem  7924  cnfcomlemOLD  7928  cnfcom3lemOLD  7932  rankelb  8019  rankval3b  8021  ackbij2lem1  8376  ackbij1lem9  8385  ackbij1lem10  8386  ackbij1lem18  8394  ackbij2lem3  8398  ackbij2  8400  fin23lem7  8473  enfin2i  8478  isf32lem9  8518  isf34lem4  8534  fin1a2lem11  8567  hsmexlem4  8586  ttukeylem6  8671  fpwwe2lem8  8792  fpwwe2lem9  8793  fpwwe2  8798  canth4  8802  intwun  8890  wuncval2  8902  inttsk  8929  rankcf  8932  r1tskina  8937  tskuni  8938  elprnq  9148  dedekind  9521  suprub  10279  suprleub  10282  supmul1  10283  supmullem1  10284  supmul  10286  infmrgelb  10298  un0addcl  10601  un0mulcl  10602  suprzcl  10709  zsupss  10932  supxrleub  11277  supxrre  11278  supxrss  11283  infmxrgelb  11285  infmxrre  11286  icoshftf1o  11395  supicc  11420  supiccub  11421  supicclub  11422  supicclub2  11423  uzindi  11787  seqcl  11810  seqfveq  11814  monoord2  11821  sermono  11822  seqsplit  11823  seqcaopr2  11826  seqf1olem2a  11828  seqf1olem2  11830  seqhomo  11837  seqz  11838  seqof2  11848  seqcoll  12200  seqcoll2  12201  ccatval1  12260  ccatass  12270  revccat  12390  rexanre  12818  rexuzre  12824  rexico  12825  limsupgle  12939  limsupval2  12942  limsupgre  12943  limsupbnd2  12945  rlim2lt  12959  rlim3  12960  ello12  12978  lo1bdd2  12986  elo12  12989  rlimclim1  13007  climrlim2  13009  lo1resb  13026  o1resb  13028  rlimcn2  13052  o1of2  13074  rlimsqzlem  13110  isercolllem3  13128  isercoll2  13130  climsup  13131  iseraltlem2  13144  summolem2a  13176  sumss  13185  fsumss  13186  fsumcvg3  13190  fsumsplit  13200  fsum2dlem  13221  fsum0diag2  13233  fsumless  13242  fsumabs  13247  fsumtscopo  13248  fsumparts  13252  fsumrlim  13257  fsumo1  13258  o1fsum  13259  fsumiun  13267  hashuni  13271  hashuniOLD  13272  ackbijnn  13274  binom1dif  13279  incexclem  13282  isumsplit  13286  isumrpcl  13289  isumless  13291  isumltss  13294  supcvg  13301  cvgrat  13326  mertenslem1  13327  rpnnen2  13491  bitsinv2  13622  bitsf1ocnv  13623  bitsinvp1  13628  eulerthlem2  13840  4sqlem11  13999  vdwlem6  14030  ramval  14052  ramcl2lem  14053  restid2  14352  mress  14514  mremre  14525  mreacs  14579  fullsubc  14743  subsubc  14746  funcres  14789  fuciso  14868  setcmon  14938  setcepi  14939  catccatid  14953  drsdirfi  15091  clatglbss  15280  ipodrsfi  15316  isacs3lem  15319  mrelatglb  15337  mrelatlub  15339  issubmnd  15432  ress0g  15433  gsumress  15487  gsumwspan  15504  frmdsssubm  15519  frmdss2  15521  grpinvssd  15583  subginv  15668  issubg2  15676  issubg4  15680  ssnmz  15703  lagsubg2  15722  resghm  15743  conjnmz  15760  conjnmzb  15761  subgga  15798  gass  15799  gasubg  15800  cntzsubm  15833  cntzmhm  15836  f1omvdmvd  15929  f1omvdconj  15932  symggen  15956  psgnunilem5  15980  psgnunilem2  15981  submod  16048  sylow1lem2  16078  sylow1lem3  16079  sylow1lem4  16080  sylow2alem2  16097  sylow2a  16098  sylow2blem2  16100  sylow3lem1  16106  sylow3lem6  16111  lsmssv  16122  lsmub2x  16126  lsmelvalm  16130  lsmcom2  16134  pj1lid  16178  pj1rid  16179  efgrelexlemb  16227  frgpup1  16252  frgpup3lem  16254  cntzcmn  16304  gsumval3eu  16361  gsumval3OLD  16362  gsumval3  16365  gsumzaddlem  16388  gsumzaddlemOLD  16390  gsumzoppg  16416  gsumzoppgOLD  16417  dprdfadd  16484  dprdfaddOLD  16491  dprdres  16499  dprdcntz2  16510  dprddisj2  16511  dprddisj2OLD  16512  dprd2dlem1  16514  dmdprdsplit2lem  16518  ablfac1lem  16543  ablfac1b  16545  ablfac1c  16546  ablfac1eu  16548  pgpfac1lem1  16549  pgpfac1lem2  16550  pgpfac1lem3  16552  pgpfac1lem4  16553  ablfaclem3  16562  rngidss  16607  invrpropd  16724  subrg1  16799  subrginv  16805  subrgunit  16807  cntzsubr  16821  abvres  16848  lssel  16941  islss3  16962  lssintcl  16967  lmhmima  17050  lmhmpreima  17051  lbsel  17081  lbspropd  17102  lsmcv  17144  lspsolvlem  17145  lbsextlem2  17162  lidlsubcl  17220  drngnidl  17233  issubassa2  17337  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  subrgascl  17512  subrgasclcl  17513  zringlpirlem1  17745  zlpirlem1  17750  regsumsupp  17894  ocvocv  17938  ocvlss  17939  pjfo  17982  ocvpj  17984  obsne0  17992  obselocv  17995  dsmmsubg  18010  frlmsslsp  18065  frlmsslspOLD  18066  ofco2  18174  mdetrsca2  18253  mdetunilem9  18268  madugsum  18291  tgclb  18417  tgidm  18427  pptbas  18454  toponmre  18539  neiptoptop  18577  neiptopnei  18578  neiptopreu  18579  clslp  18594  tgrest  18605  perfopn  18631  ordtbas  18638  ordtrest2lem  18649  pnrmcld  18788  ist1-3  18795  isreg2  18823  cncmp  18837  cmpsublem  18844  tgcmp  18846  cmpcld  18847  hauscmplem  18851  2ndcomap  18904  1stcelcls  18907  restlly  18929  lly1stc  18942  kgentopon  18953  llycmpkgen2  18965  txcls  19019  ptclsg  19030  txcnp  19035  txdis1cn  19050  txcmplem1  19056  txkgen  19067  xkoptsub  19069  xkopt  19070  xkococnlem  19074  xkoinjcn  19102  basqtop  19126  tgqtop  19127  kqfvima  19145  kqreglem1  19156  fbelss  19248  fbssfi  19252  fgabs  19294  trfg  19306  uffixfr  19338  uffixsn  19340  elfm2  19363  fmfnfmlem4  19372  fmfnfm  19373  flimnei  19382  flimrest  19398  flimcls  19400  flimsncls  19401  flffbas  19410  fclsrest  19439  fclscmp  19445  alexsublem  19458  ptcmplem3  19468  ptcmplem4  19469  cnextfres  19482  subgntr  19519  opnsubg  19520  clssubg  19521  tgpconcomp  19525  divstgpopn  19532  divstgplem  19533  tsmssubm  19558  tgptsmscls  19566  tgptsmscld  19567  tsmsxplem1  19569  tsmsxplem2  19570  ustssxp  19621  ustuqtop4  19661  utopsnneiplem  19664  utop2nei  19667  isucn2  19696  ucnima  19698  psmetres2  19732  imasdsf1olem  19790  blpnfctr  19853  xmetresbl  19854  mopni2  19910  mopni3  19911  rnblopn  19916  metustexhalfOLD  19980  metustexhalf  19981  metutopOLD  19999  psmetutop  20000  tgioo  20215  xrsmopn  20231  zdis  20235  icccmplem3  20243  reconnlem2  20246  opnreen  20250  metdsf  20266  metdsge  20267  metdsle  20270  metdsre  20271  metnrmlem2  20278  metnrmlem3  20279  fsumcn  20288  climcncf  20318  icccvx  20364  cnheibor  20369  bndth  20372  lebnumlem1  20375  lebnumlem2  20376  pi1grplem  20463  clmneg  20495  nmoleub2lem3  20512  cphsqrcl  20545  cphabscl  20546  clsocv  20604  iscfil2  20619  cfil3i  20622  cfilfcls  20627  cmetcaulem  20641  iscmet3lem2  20645  cfilresi  20648  caussi  20650  lmclim  20655  rrxnm  20737  rrxcph  20738  rrxmval  20746  rrxmetlem  20748  rrxmet  20749  rrxdstprj1  20750  minveclem1  20753  minveclem3b  20757  minveclem4  20761  minveclem6  20763  pjthlem2  20767  ivth2  20781  ivthicc  20784  ovollb2lem  20813  ovoliunlem1  20827  ovolicc2lem4  20845  ioombl1lem4  20884  dyadmax  20920  dyadmbl  20922  opnmbllem  20923  volsup2  20927  volivth  20929  vitalilem5  20934  i1fima  20998  i1fd  21001  itg1val2  21004  itg1cl  21005  itg1ge0  21006  itg11  21011  i1fadd  21015  i1fmul  21016  itg1addlem4  21019  itg1addlem5  21020  i1fmulc  21023  itg1mulc  21024  itg10a  21030  itg1ge0a  21031  itg1climres  21034  mbfi1fseqlem4  21038  mbfi1fseqlem5  21039  mbfi1flim  21043  mbfmullem2  21044  itg2const2  21061  itg2splitlem  21068  itg2split  21069  itg2gt0  21080  itg2cnlem2  21082  iblss  21124  iblss2  21125  itgss3  21134  itgless  21136  itgfsum  21146  itgsplit  21155  itgsplitioo  21157  itggt0  21161  itgcn  21162  ditgcl  21175  ditgswap  21176  ditgsplitlem  21177  ellimc3  21196  perfdvf  21220  dvreslem  21226  dvcnp  21235  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvcjbr  21265  dvmptfsum  21289  dvcnvlem  21290  dvlip  21307  dvlipcn  21308  dvlip2  21309  dv11cn  21315  dvivthlem1  21322  dvivthlem2  21323  dvne0  21325  lhop1lem  21327  lhop2  21329  lhop  21330  dvcvx  21334  dvfsumle  21335  dvfsumge  21336  dvfsumabs  21337  dvfsumlem2  21341  dvfsumlem3  21342  dvfsumrlimge0  21344  dvfsumrlim2  21346  ftc1lem1  21349  ftc1lem4  21353  ftc1lem6  21355  itgsubstlem  21362  ig1peu  21528  plyeq0lem  21563  plypf1  21565  coeeulem  21577  vieta1lem1  21661  vieta1lem2  21662  plyexmo  21664  taylthlem1  21723  taylthlem2  21724  ulmdvlem1  21750  ulmdvlem3  21752  mtest  21754  radcnv0  21766  pserulm  21772  psercnlem2  21774  psercnlem1  21775  psercn  21776  pserdvlem1  21777  pserdvlem2  21778  pserdv  21779  pserdv2  21780  abelthlem3  21783  abelthlem4  21784  abelthlem9  21790  pige3  21864  efif1olem4  21886  efopnlem2  21987  efopn  21988  logccv  21993  loglesqr  22081  rlimcnp  22244  rlimcnp2  22245  xrlimcnp  22247  efrlim  22248  jensenlem1  22265  jensenlem2  22266  jensen  22267  fsumharmonic  22290  wilthlem2  22292  basellem3  22305  basellem5  22307  chtdif  22381  sqff1o  22405  musumsum  22417  muinv  22418  chtublem  22435  fsumvma  22437  vmasum  22440  chpval2  22442  chpchtsum  22443  chpub  22444  perfectlem2  22454  lgsquadlem2  22579  chebbnd1lem1  22603  dchrisumlem2  22624  dchrisumlem3  22625  dchrmusum2  22628  dchrisum0fno1  22645  rpvmasum2  22646  dchrisum0lem1b  22649  dchrisum0lem1  22650  rplogsum  22661  mudivsum  22664  mulogsum  22666  mulog2sumlem2  22669  selberg2lem  22684  chpdifbndlem1  22687  pntrlog2bndlem6  22717  pntrlog2bnd  22718  pntlemj  22737  pntlemf  22739  pntlem3  22743  tglineelsb2  22909  tglinecom  22912  axlowdimlem13  23023  axlowdimlem16  23026  axcontlem4  23036  axcontlem10  23042  umgraex  23080  redwlk  23328  eupares  23419  subgoinv  23618  ubthlem1  24094  ubthlem2  24095  ubthlem3  24096  minvecolem1  24098  minvecolem4  24104  minvecolem5  24105  minvecolem6  24106  shel  24436  chel  24456  ocorth  24517  pjpreeq  24624  chscllem1  24863  chscllem2  24864  spansncvi  24878  off2  25783  xppreima  25788  ofpreima  25808  ofpreima2  25809  fcnvgreu  25815  supxrnemnf  25879  ssnnssfz  25899  iundisjfi  25903  hashunif  25907  toslublem  25951  tosglblem  25953  gsumvsca1  26104  gsumvsca2  26105  ress1r  26110  tpr2rico  26196  ordtrest2NEWlem  26206  ordtconlem1  26208  fsumcvg4  26234  indsum  26333  esummono  26363  gsumesum  26364  elsigass  26422  elsigagen  26444  measiuns  26485  measres  26490  volmeas  26501  sibfof  26574  sitgclg  26576  eulerpartlemsv2  26589  eulerpartlemsf  26590  eulerpartlemsv3  26592  eulerpartlemgc  26593  eulerpartlemv  26595  eulerpartlemb  26599  eulerpartlemf  26601  eulerpartlemr  26605  eulerpartlemgvv  26607  eulerpartlemgu  26608  eulerpartlemgs2  26611  ballotlemsel1i  26743  ballotlemsima  26746  ballotlemfrceq  26759  signsplypnf  26799  signsply0  26800  signstcl  26814  signstf  26815  signstfvn  26818  signstfvp  26820  signsvfn  26831  lgamgulmlem2  26864  lgamgulm2  26870  lgambdd  26871  erdszelem8  26934  cvmscld  27010  cvmsss2  27011  cvmopnlem  27015  cvmlift2lem9  27048  cvmlift2lem11  27050  cvmlift2lem12  27051  cvmliftpht  27055  clim2prod  27250  prodfn0  27256  prodfrec  27257  prodmolem2a  27294  fprodntriv  27302  prodss  27307  fprodss  27308  fprodsplit  27323  fprod2dlem  27338  binomfallfaclem2  27390  trpredelss  27543  sltres  27652  nobndup  27688  nobnddown  27689  nofulllem5  27694  bpolycl  28042  bpolysum  28043  bpolydiflem  28044  supaddc  28261  supadd  28262  opnmbllem0  28271  mblfinlem2  28273  ismblfin  28276  cnambfre  28284  itg2addnclem2  28288  ftc1cnnclem  28309  ftc1cnnc  28310  ftc1anclem6  28316  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  ftc2nc  28320  areacirclem2  28329  areacirclem4  28331  areacirc  28333  opnrebl2  28360  fnessex  28391  fneuni  28392  comppfsc  28423  neibastop1  28424  neibastop2lem  28425  neibastop3  28427  sdclem1  28483  mettrifi  28497  sstotbnd2  28517  equivtotbnd  28521  isbndx  28525  totbndbnd  28532  equivbnd2  28535  cntotbnd  28539  heibor1lem  28552  heiborlem3  28556  heibor  28564  iccbnd  28583  idlcl  28661  divrngidl  28672  ismrcd1  28879  mzpf  28917  mzpindd  28927  fphpdo  29001  pell14qrre  29043  pell14qrne0  29044  elpell14qr2  29048  elpell1qr2  29058  pellfundex  29072  dnnumch3lem  29244  dnnumch3  29245  fnwe2lem2  29249  aomclem4  29255  kelac1  29261  kercvrlsm  29281  hbtlem2  29325  hbtlem5  29329  flcidc  29376  cntzsdrg  29404  itgpowd  29435  fmul01  29606  fmulcl  29607  climinf  29625  ibliccsinexp  29637  iblioosinexp  29639  stoweidlem5  29646  stoweidlem7  29648  stoweidlem11  29652  stoweidlem17  29658  stoweidlem18  29659  stoweidlem26  29667  stoweidlem27  29668  stoweidlem31  29672  stoweidlem35  29676  stoweidlem39  29680  stoweidlem42  29683  stoweidlem43  29684  stoweidlem44  29685  stoweidlem48  29689  stoweidlem51  29692  stoweidlem52  29693  stoweidlem56  29697  stoweidlem57  29698  stoweidlem59  29700  stoweidlem60  29701  stoweidlem61  29702  elfzom1elfzo  30063  zpnn0elfzo  30067  wwlkm1edg  30213  clwlkisclwwlklem2fv1  30290  clwlkisclwwlklem1  30295  clwwlkvbij  30309  clwwisshclwwlem  30316  clwlkfclwwlk  30363  lincresunit3  30724  bnj1137  31688  bnj1498  31754  lsatfixedN  32227  elpaddn0  33017  diaintclN  34276  dibglbN  34384  dibintclN  34385  dihrnlss  34495  dihglblem3N  34513  dihglblem6  34558  dihintcl  34562  dochkr1  34696  dochkr1OLDN  34697  lcfrlem5  34764  lcfr  34803  mapdrvallem2  34863  hgmapvvlem3  35146  hdmapoc  35152  hlhilocv  35178
  Copyright terms: Public domain W3C validator