Theorem releqi 5727

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

Syntax hints:   ↔ wb 206   = wceq 1541  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-rel 5631

This theorem is referenced by:  reluni  5767  relint  5768  reldmmpo  7492  frrlem6  8233  tfrlem6  8313  relsdom  8890  0rest  17349  firest  17352  2oppchomf  17647  oppchofcl  18183  oyoncl  18193  releqg  19104  reldvdsr  20296  restbas  23102  hlimcaui  31311  gonan0  35586  satffunlem2lem2  35600  relbigcup  36089  fnsingle  36111  funimage  36120  colinrel  36251  brcnvrabga  38535  relcoels  38687  iscard4  43774  neicvgnvor  44357  xlimrel  46064  tposideq2  49134  reldmxpc  49491  reldmprcof1  49626  reldmlmd2  49898  reldmcmd2  49899  rellmd  49904  relcmd  49905