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

Theorem releqi 4923
 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 4922 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:   wb 189   wceq 1452   wrel 4844 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451 This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404  df-rel 4846 This theorem is referenced by:  reliun  4959  reluni  4961  relint  4962  reldmmpt2  6426  wfrrel  7059  tfrlem6  7118  relsdom  7594  cda1dif  8624  0rest  15406  firest  15409  2oppchomf  15707  oppchofcl  16223  oyoncl  16233  releqg  16942  reldvdsr  17950  restbas  20251  hlimcaui  26970  relbigcup  30735  fnsingle  30757  funimage  30766  colinrel  30895
 Copyright terms: Public domain W3C validator