Theorem releqi 5750

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

Syntax hints:   ↔ wb 208   = wceq 1560  Rel wrel 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921  df-rel 5654

This theorem is referenced by:  reluni  5791  relint  5792  reldmmpo  7530  frrlem6  8272  tfrlem6OLD  8353  relsdom  8934  0rest  17458  firest  17461  2oppchomf  17756  oppchofcl  18292  oyoncl  18302  releqg  19216  reldvdsr  20409  restbas  23218  hlimcaui  31439  gonan0  35742  satffunlem2lem2  35756  relbigcup  36245  fnsingle  36267  funimage  36276  colinrel  36407  brcnvrabga  38841  relqmap  38951  relcoels  39013  iscard4  44109  neicvgnvor  44692  xlimrel  46394  tposideq2  49510  reldmxpc  49867  reldmprcof1  50002  reldmlmd2  50274  reldmcmd2  50275  rellmd  50280  relcmd  50281