Theorem releqi 5728

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

Syntax hints:   ↔ wb 206   = wceq 1542  Rel wrel 5630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-rel 5632

This theorem is referenced by:  reluni  5768  relint  5769  reldmmpo  7495  frrlem6  8235  tfrlem6  8315  relsdom  8894  0rest  17386  firest  17389  2oppchomf  17684  oppchofcl  18220  oyoncl  18230  releqg  19144  reldvdsr  20334  restbas  23136  hlimcaui  31325  gonan0  35593  satffunlem2lem2  35607  relbigcup  36096  fnsingle  36118  funimage  36127  colinrel  36258  brcnvrabga  38680  relqmap  38790  relcoels  38852  iscard4  43981  neicvgnvor  44564  xlimrel  46269  tposideq2  49379  reldmxpc  49736  reldmprcof1  49871  reldmlmd2  50143  reldmcmd2  50144  rellmd  50149  relcmd  50150