Theorem releqi 5721

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

Syntax hints:   ↔ wb 207   = wceq 1547  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900  df-rel 5625

This theorem is referenced by:  reluni  5761  relint  5762  reldmmpo  7490  frrlem6  8231  tfrlem6  8311  relsdom  8890  0rest  17383  firest  17386  2oppchomf  17681  oppchofcl  18217  oyoncl  18227  releqg  19141  reldvdsr  20331  restbas  23141  hlimcaui  31325  gonan0  35620  satffunlem2lem2  35634  relbigcup  36123  fnsingle  36145  funimage  36154  colinrel  36285  brcnvrabga  38709  relqmap  38819  relcoels  38881  iscard4  43977  neicvgnvor  44560  xlimrel  46263  tposideq2  49379  reldmxpc  49736  reldmprcof1  49871  reldmlmd2  50143  reldmcmd2  50144  rellmd  50149  relcmd  50150