Theorem releqi 5801

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

Syntax hints:   ↔ wb 206   = wceq 1537  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-rel 5707

This theorem is referenced by:  reliun  5840  reluni  5842  relint  5843  reldmmpo  7584  frrlem6  8332  wfrrelOLD  8370  tfrlem6  8438  relsdom  9010  0rest  17489  firest  17492  2oppchomf  17784  oppchofcl  18330  oyoncl  18340  releqg  19215  reldvdsr  20386  restbas  23187  hlimcaui  31268  gonan0  35360  satffunlem2lem2  35374  relbigcup  35861  fnsingle  35883  funimage  35892  colinrel  36021  brcnvrabga  38298  relcoels  38380  iscard4  43495  neicvgnvor  44078  xlimrel  45741