Theorem releqi 5740

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-rel 5645

This theorem is referenced by:  reliun  5779  reluni  5781  relint  5782  reldmmpo  7523  frrlem6  8270  tfrlem6  8350  relsdom  8925  0rest  17392  firest  17395  2oppchomf  17685  oppchofcl  18221  oyoncl  18231  releqg  19107  reldvdsr  20269  restbas  23045  hlimcaui  31165  gonan0  35379  satffunlem2lem2  35393  relbigcup  35885  fnsingle  35907  funimage  35916  colinrel  36045  brcnvrabga  38324  relcoels  38415  iscard4  43522  neicvgnvor  44105  xlimrel  45818  tposideq2  48877  reldmxpc  49235  reldmprcof1  49370  reldmlmd2  49642  reldmcmd2  49643  rellmd  49648  relcmd  49649