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

Theorem releqi 5787
Description: Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
Hypothesis
Ref Expression
releqi.1 𝐴 = 𝐵
Assertion
Ref Expression
releqi (Rel 𝐴 ↔ Rel 𝐵)

Proof of Theorem releqi
StepHypRef Expression
1 releqi.1 . 2 𝐴 = 𝐵
2 releq 5786 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2ax-mp 5 1 (Rel 𝐴 ↔ Rel 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1540  Rel wrel 5690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-rel 5692
This theorem is referenced by:  reliun  5826  reluni  5828  relint  5829  reldmmpo  7567  frrlem6  8316  wfrrelOLD  8354  tfrlem6  8422  relsdom  8992  0rest  17474  firest  17477  2oppchomf  17767  oppchofcl  18305  oyoncl  18315  releqg  19193  reldvdsr  20360  restbas  23166  hlimcaui  31255  gonan0  35397  satffunlem2lem2  35411  relbigcup  35898  fnsingle  35920  funimage  35929  colinrel  36058  brcnvrabga  38343  relcoels  38425  iscard4  43546  neicvgnvor  44129  xlimrel  45835  tposideq2  48789  reldmxpc  48952
  Copyright terms: Public domain W3C validator