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

Theorem releqd 5092
Description: Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
Hypothesis
Ref Expression
releqd.1
Assertion
Ref Expression
releqd

Proof of Theorem releqd
StepHypRef Expression
1 releqd.1 . 2
2 releq 5090 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  Relwrel 5009
This theorem is referenced by:  dftpos3  6992  tposfo2  6997  tposf12  6999  imasaddfnlem  14925  imasvscafn  14934  joindmss  15637  meetdmss  15651  mattpostpos  18956  cnextrel  20563  perpln1  24087  perpln2  24088  relfae  28219  cicer  32590  dibvalrel  36890  dicvalrelN  36912  diclspsn  36921  dihvalrel  37006  dih1  37013  dihmeetlem4preN  37033
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