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

Theorem releqi 5236
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 5235 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2ax-mp 5 1 (Rel 𝐴 ↔ Rel 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1523  Rel wrel 5148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-rel 5150
This theorem is referenced by:  reliun  5272  reluni  5274  relint  5275  reldmmpt2  6813  wfrrel  7465  tfrlem6  7523  relsdom  8004  cda1dif  9036  0rest  16137  firest  16140  2oppchomf  16431  oppchofcl  16947  oyoncl  16957  releqg  17688  reldvdsr  18690  restbas  21010  hlimcaui  28221  frrlem6  31914  relbigcup  32129  fnsingle  32151  funimage  32160  colinrel  32289  relcoels  34319  neicvgnvor  38731  xlimrel  40364
  Copyright terms: Public domain W3C validator