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

Theorem releqi 5091
Description: Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
Hypothesis
Ref Expression
releqi.1
Assertion
Ref Expression
releqi

Proof of Theorem releqi
StepHypRef Expression
1 releqi.1 . 2
2 releq 5090 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  =wceq 1395  Relwrel 5009
This theorem is referenced by:  reliun  5128  reluni  5130  relint  5131  reldmmpt2  6413  tfrlem6  7070  relsdom  7543  cda1dif  8577  0rest  14827  firest  14830  2oppchomf  15119  oppchofcl  15529  oyoncl  15539  releqg  16248  reldvdsr  17293  eltopspOLD  19419  restbas  19659  hlimcaui  26154  wfrlem6  29348  relbigcup  29547  fnsingle  29569  funimage  29578  colinrel  29707
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