Theorem releqi 5725

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916  df-rel 5629

This theorem is referenced by:  reluni  5765  relint  5766  reldmmpo  7490  frrlem6  8231  tfrlem6  8311  relsdom  8888  0rest  17347  firest  17350  2oppchomf  17645  oppchofcl  18181  oyoncl  18191  releqg  19102  reldvdsr  20294  restbas  23100  hlimcaui  31260  gonan0  35535  satffunlem2lem2  35549  relbigcup  36038  fnsingle  36060  funimage  36069  colinrel  36200  brcnvrabga  38474  relcoels  38626  iscard4  43716  neicvgnvor  44299  xlimrel  46006  tposideq2  49076  reldmxpc  49433  reldmprcof1  49568  reldmlmd2  49840  reldmcmd2  49841  rellmd  49846  relcmd  49847