Theorem releqi 5743

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

Syntax hints:   ↔ wb 206   = wceq 1540  Rel wrel 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-rel 5648

This theorem is referenced by:  reliun  5782  reluni  5784  relint  5785  reldmmpo  7526  frrlem6  8273  tfrlem6  8353  relsdom  8928  0rest  17399  firest  17402  2oppchomf  17692  oppchofcl  18228  oyoncl  18238  releqg  19114  reldvdsr  20276  restbas  23052  hlimcaui  31172  gonan0  35386  satffunlem2lem2  35400  relbigcup  35892  fnsingle  35914  funimage  35923  colinrel  36052  brcnvrabga  38331  relcoels  38422  iscard4  43529  neicvgnvor  44112  xlimrel  45825  tposideq2  48881  reldmxpc  49239  reldmprcof1  49374  reldmlmd2  49646  reldmcmd2  49647  rellmd  49652  relcmd  49653