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

Theorem releqi 5405
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 5404 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2ax-mp 5 1 (Rel 𝐴 ↔ Rel 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 198   = wceq 1653  Rel wrel 5315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781  df-rel 5317
This theorem is referenced by:  reliun  5441  reluni  5443  relint  5444  reldmmpt2  7003  wfrrel  7657  tfrlem6  7715  relsdom  8200  cda1dif  9284  0rest  16401  firest  16404  2oppchomf  16694  oppchofcl  17211  oyoncl  17221  releqg  17950  reldvdsr  18956  restbas  21287  hlimcaui  28609  frrlem6  32293  relbigcup  32508  fnsingle  32530  funimage  32539  colinrel  32668  cnfinltrel  33730  brcnvrabga  34595  relcoels  34664  neicvgnvor  39183  xlimrel  40777
  Copyright terms: Public domain W3C validator