Theorem releqi 5765

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

Syntax hints:   ↔ wb 209   = wceq 1567  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-rel 5669

This theorem is referenced by:  reluni  5806  relint  5807  reldmmpo  7545  frrlem6  8287  tfrlem6OLD  8368  relsdom  8949  0rest  17481  firest  17484  2oppchomf  17779  oppchofcl  18315  oyoncl  18325  releqg  19240  reldvdsr  20441  restbas  23283  hlimcaui  31528  gonan0  35782  satffunlem2lem2  35796  relbigcup  36285  fnsingle  36307  funimage  36316  colinrel  36447  brcnvrabga  38880  relqmap  38990  relcoels  39052  iscard4  44150  neicvgnvor  44733  xlimrel  46425  tposideq2  49551  reldmxpc  49908  reldmprcof1  50043  reldmlmd2  50315  reldmcmd2  50316  rellmd  50321  relcmd  50322