Theorem releqi 5616

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

Syntax hints:   ↔ wb 209   = wceq 1538  Rel wrel 5524

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-rel 5526

This theorem is referenced by:  reliun  5653  reluni  5655  relint  5656  reldmmpo  7264  wfrrel  7943  tfrlem6  8001  relsdom  8499  0rest  16695  firest  16698  2oppchomf  16986  oppchofcl  17502  oyoncl  17512  releqg  18319  reldvdsr  19390  restbas  21763  hlimcaui  29019  gonan0  32752  satffunlem2lem2  32766  frrlem6  33241  relbigcup  33471  fnsingle  33493  funimage  33502  colinrel  33631  brcnvrabga  35759  relcoels  35829  iscard4  40241  neicvgnvor  40819  xlimrel  42462