Theorem releqi 5753

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896  df-rel 5657

This theorem is used by:  reluni  5795  relint  5796  reldmmpo  7554  frrlem6  8309  tfrlem6OLD  8390  relsdom  8980  0rest  17600  firest  17603  2oppchomf  17898  oppchofcl  18434  oyoncl  18444  releqg  19385  reldvdsr  20590  restbas  23476  hlimcaui  31838  gonan0  36199  satffunlem2lem2  36213  relbigcup  36701  fnsingle  36723  funimage  36732  colinrel  36864  brcnvrabga  39317  relqmap  39427  relcoels  39489  iscard4  44577  neicvgnvor  45159  xlimrel  46873  tposideq2  50040  reldmxpc  50397  reldmprcof1  50532  reldmlmd2  50804  reldmcmd2  50805  rellmd  50810  relcmd  50811