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

Theorem releqi 5645
 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 5644 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2ax-mp 5 1 (Rel 𝐴 ↔ Rel 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 208   = wceq 1530  Rel wrel 5553 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-in 3941  df-ss 3950  df-rel 5555 This theorem is referenced by:  reliun  5682  reluni  5684  relint  5685  reldmmpo  7277  wfrrel  7952  tfrlem6  8010  relsdom  8508  0rest  16695  firest  16698  2oppchomf  16986  oppchofcl  17502  oyoncl  17512  releqg  18319  reldvdsr  19386  restbas  21758  hlimcaui  29005  gonan0  32627  satffunlem2lem2  32641  frrlem6  33116  relbigcup  33346  fnsingle  33368  funimage  33377  colinrel  33506  brcnvrabga  35586  relcoels  35656  iscard4  39885  neicvgnvor  40451  xlimrel  42085
 Copyright terms: Public domain W3C validator