Theorem releqi 5732

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-rel 5638

This theorem is referenced by:  reliun  5770  reluni  5772  relint  5773  reldmmpo  7503  frrlem6  8247  tfrlem6  8327  relsdom  8902  0rest  17368  firest  17371  2oppchomf  17661  oppchofcl  18197  oyoncl  18207  releqg  19083  reldvdsr  20245  restbas  23021  hlimcaui  31138  gonan0  35352  satffunlem2lem2  35366  relbigcup  35858  fnsingle  35880  funimage  35889  colinrel  36018  brcnvrabga  38297  relcoels  38388  iscard4  43495  neicvgnvor  44078  xlimrel  45791  tposideq2  48850  reldmxpc  49208  reldmprcof1  49343  reldmlmd2  49615  reldmcmd2  49616  rellmd  49621  relcmd  49622