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

Theorem releqi 4960
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 4959 . 2  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )
31, 2ax-mp 8 1  |-  ( Rel 
A  <->  Rel  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    = wceq 1652   Rel wrel 4883
This theorem is referenced by:  reliun  4995  reluni  4997  relint  4998  reldmmpt2  6181  tfrlem6  6643  relsdom  7116  cda1dif  8056  0rest  13657  firest  13660  2oppchomf  13950  oppchofcl  14357  oyoncl  14367  releqg  14987  reldvdsr  15749  eltopspOLD  16983  restbas  17222  hlimcaui  22739  wfrlem6  25543  relbigcup  25742  fnsingle  25764  funimage  25773  colinrel  25991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334  df-rel 4885
  Copyright terms: Public domain W3C validator