Theorem releqi 5787

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

Syntax hints:   ↔ wb 206   = wceq 1540  Rel wrel 5690

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-rel 5692

This theorem is referenced by:  reliun  5826  reluni  5828  relint  5829  reldmmpo  7567  frrlem6  8316  wfrrelOLD  8354  tfrlem6  8422  relsdom  8992  0rest  17474  firest  17477  2oppchomf  17767  oppchofcl  18305  oyoncl  18315  releqg  19193  reldvdsr  20360  restbas  23166  hlimcaui  31255  gonan0  35397  satffunlem2lem2  35411  relbigcup  35898  fnsingle  35920  funimage  35929  colinrel  36058  brcnvrabga  38343  relcoels  38425  iscard4  43546  neicvgnvor  44129  xlimrel  45835  tposideq2  48789  reldmxpc  48952