Theorem releqi 5790

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

Syntax hints:   ↔ wb 206   = wceq 1537  Rel wrel 5694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-rel 5696

This theorem is referenced by:  reliun  5829  reluni  5831  relint  5832  reldmmpo  7567  frrlem6  8315  wfrrelOLD  8353  tfrlem6  8421  relsdom  8991  0rest  17476  firest  17479  2oppchomf  17771  oppchofcl  18317  oyoncl  18327  releqg  19206  reldvdsr  20377  restbas  23182  hlimcaui  31265  gonan0  35377  satffunlem2lem2  35391  relbigcup  35879  fnsingle  35901  funimage  35910  colinrel  36039  brcnvrabga  38324  relcoels  38406  iscard4  43523  neicvgnvor  44106  xlimrel  45776