Theorem releqi 5777

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

Step	Hyp	Ref	Expression
1		releqi.1	. 2 ⊢ 𝐴 = 𝐵
2		releq 5776	. 2 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (Rel 𝐴 ↔ Rel 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1541  Rel wrel 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-rel 5683

This theorem is referenced by:  reliun  5816  reluni  5818  relint  5819  reldmmpo  7545  frrlem6  8278  wfrrelOLD  8316  tfrlem6  8384  relsdom  8948  0rest  17379  firest  17382  2oppchomf  17674  oppchofcl  18217  oyoncl  18227  releqg  19091  reldvdsr  20251  restbas  22882  hlimcaui  30744  gonan0  34669  satffunlem2lem2  34683  relbigcup  35161  fnsingle  35183  funimage  35192  colinrel  35321  brcnvrabga  37514  relcoels  37597  iscard4  42586  neicvgnvor  43169  xlimrel  44835