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

Theorem relss 5095
Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58. (Contributed by NM, 15-Aug-1994.)
Assertion
Ref Expression
relss

Proof of Theorem relss
StepHypRef Expression
1 sstr2 3510 . 2
2 df-rel 5011 . 2
3 df-rel 5011 . 2
41, 2, 33imtr4g 270 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4   cvv 3109  C_wss 3475  X.cxp 5002  Relwrel 5009
This theorem is referenced by:  relin1  5125  relin2  5126  reldif  5127  relres  5306  iss  5326  cnvdif  5417  difxp  5436  sofld  5460  funss  5611  funssres  5633  fliftcnv  6209  fliftfun  6210  frxp  6910  reltpos  6979  tpostpos  6994  swoer  7358  erinxp  7404  sbthcl  7659  fpwwe2lem8  9036  fpwwe2lem9  9037  fpwwe2lem12  9040  recmulnq  9363  prcdnq  9392  ltrel  9670  lerel  9672  dfle2  11382  dflt2  11383  pwsle  14889  isinv  15154  invsym2  15157  invfun  15158  oppcsect2  15169  oppcinv  15170  relfull  15277  relfth  15278  psss  15844  gicer  16324  gsum2d  16999  gsum2dOLD  17000  isunit  17306  opsrtoslem2  18149  txdis1cn  20136  hmpher  20285  tgphaus  20615  qustgplem  20619  tsmsxp  20657  xmeter  20936  ovoliunlem1  21913  taylf  22756  lgsquadlem1  23629  lgsquadlem2  23630  nvrel  25495  phrel  25730  bnrel  25783  hlrel  25806  elrn3  29192  sscoid  29563  heicant  30049  trer  30134  fneer  30171  dvhopellsm  36844  diclspsn  36921  dih1dimatlem  37056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-rel 5011
  Copyright terms: Public domain W3C validator