Theorem releqi 5766

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

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

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-rel 5670

This theorem is used by:  reluni  5807  relint  5808  reldmmpo  7553  frrlem6  8294  tfrlem6OLD  8375  relsdom  8956  0rest  17506  firest  17509  2oppchomf  17804  oppchofcl  18340  oyoncl  18350  releqg  19287  reldvdsr  20490  restbas  23367  hlimcaui  31661  gonan0  35923  satffunlem2lem2  35937  relbigcup  36426  fnsingle  36448  funimage  36457  colinrel  36588  brcnvrabga  39051  relqmap  39161  relcoels  39223  iscard4  44319  neicvgnvor  44902  xlimrel  46594  tposideq2  49726  reldmxpc  50083  reldmprcof1  50218  reldmlmd2  50490  reldmcmd2  50491  rellmd  50496  relcmd  50497