Theorem releqi 5756

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-rel 5661

This theorem is referenced by:  reliun  5795  reluni  5797  relint  5798  reldmmpo  7541  frrlem6  8290  wfrrelOLD  8328  tfrlem6  8396  relsdom  8966  0rest  17443  firest  17446  2oppchomf  17736  oppchofcl  18272  oyoncl  18282  releqg  19158  reldvdsr  20320  restbas  23096  hlimcaui  31217  gonan0  35414  satffunlem2lem2  35428  relbigcup  35915  fnsingle  35937  funimage  35946  colinrel  36075  brcnvrabga  38360  relcoels  38442  iscard4  43557  neicvgnvor  44140  xlimrel  45849  tposideq2  48864  reldmxpc  49163  reldmprcof1  49291  reldmlmd2  49525  reldmcmd2  49526  rellmd  49529  relcmd  49530