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

Theorem releqi 4937
Description: Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
Hypothesis
Ref Expression
releqi.1  |-  A  =  B
Assertion
Ref Expression
releqi  |-  ( Rel 
A  <->  Rel  B )

Proof of Theorem releqi
StepHypRef Expression
1 releqi.1 . 2  |-  A  =  B
2 releq 4936 . 2  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )
31, 2ax-mp 5 1  |-  ( Rel 
A  <->  Rel  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437   Rel wrel 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-rel 4860
This theorem is referenced by:  reliun  4973  reluni  4975  relint  4976  reldmmpt2  6421  wfrrel  7052  tfrlem6  7111  relsdom  7587  cda1dif  8613  0rest  15327  firest  15330  2oppchomf  15628  oppchofcl  16144  oyoncl  16154  releqg  16863  reldvdsr  17871  restbas  20172  hlimcaui  26887  relbigcup  30669  fnsingle  30691  funimage  30700  colinrel  30829
  Copyright terms: Public domain W3C validator