Theorem releqi 5688

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

Syntax hints:   ↔ wb 205   = wceq 1539  Rel wrel 5594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-rel 5596

This theorem is referenced by:  reliun  5726  reluni  5728  relint  5729  reldmmpo  7408  frrlem6  8107  wfrrelOLD  8145  tfrlem6  8213  relsdom  8740  0rest  17140  firest  17143  2oppchomf  17435  oppchofcl  17978  oyoncl  17988  releqg  18803  reldvdsr  19886  restbas  22309  hlimcaui  29598  gonan0  33354  satffunlem2lem2  33368  relbigcup  34199  fnsingle  34221  funimage  34230  colinrel  34359  brcnvrabga  36477  relcoels  36547  iscard4  41140  neicvgnvor  41726  xlimrel  43361