Theorem releqi 5717

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

Syntax hints:   ↔ wb 206   = wceq 1541  Rel wrel 5619

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 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914  df-rel 5621

This theorem is referenced by:  reliun  5755  reluni  5757  relint  5758  reldmmpo  7480  frrlem6  8221  tfrlem6  8301  relsdom  8876  0rest  17333  firest  17336  2oppchomf  17630  oppchofcl  18166  oyoncl  18176  releqg  19087  reldvdsr  20278  restbas  23073  hlimcaui  31216  gonan0  35436  satffunlem2lem2  35450  relbigcup  35939  fnsingle  35961  funimage  35970  colinrel  36101  brcnvrabga  38384  relcoels  38536  iscard4  43636  neicvgnvor  44219  xlimrel  45928  tposideq2  48999  reldmxpc  49357  reldmprcof1  49492  reldmlmd2  49764  reldmcmd2  49765  rellmd  49770  relcmd  49771