Theorem releqi 5758

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916  df-rel 5662

This theorem is used by:  reluni  5799  relint  5800  reldmmpo  7548  frrlem6  8291  tfrlem6OLD  8372  relsdom  8960  0rest  17515  firest  17518  2oppchomf  17813  oppchofcl  18349  oyoncl  18359  releqg  19299  reldvdsr  20502  restbas  23384  hlimcaui  31718  gonan0  35972  satffunlem2lem2  35986  relbigcup  36475  fnsingle  36497  funimage  36506  colinrel  36638  brcnvrabga  39091  relqmap  39201  relcoels  39263  iscard4  44374  neicvgnvor  44957  xlimrel  46649  tposideq2  49816  reldmxpc  50173  reldmprcof1  50308  reldmlmd2  50580  reldmcmd2  50581  rellmd  50586  relcmd  50587