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 1540  Rel wrel 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-rel 5683

This theorem is referenced by:  reliun  5816  reluni  5818  relint  5819  reldmmpo  7546  frrlem6  8282  wfrrelOLD  8320  tfrlem6  8388  relsdom  8952  0rest  17382  firest  17385  2oppchomf  17677  oppchofcl  18223  oyoncl  18233  releqg  19098  reldvdsr  20258  restbas  22982  hlimcaui  30923  gonan0  34848  satffunlem2lem2  34862  relbigcup  35340  fnsingle  35362  funimage  35371  colinrel  35500  brcnvrabga  37677  relcoels  37760  iscard4  42749  neicvgnvor  43332  xlimrel  44997