Theorem releqi 5678

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 5677	. 2 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (Rel 𝐴 ↔ Rel 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1539  Rel wrel 5585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-rel 5587

This theorem is referenced by:  reliun  5715  reluni  5717  relint  5718  reldmmpo  7386  frrlem6  8078  wfrrelOLD  8116  tfrlem6  8184  relsdom  8698  0rest  17057  firest  17060  2oppchomf  17352  oppchofcl  17894  oyoncl  17904  releqg  18718  reldvdsr  19801  restbas  22217  hlimcaui  29499  gonan0  33254  satffunlem2lem2  33268  relbigcup  34126  fnsingle  34148  funimage  34157  colinrel  34286  brcnvrabga  36404  relcoels  36474  iscard4  41038  neicvgnvor  41615  xlimrel  43251