Theorem releqi 5405

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

Syntax hints:   ↔ wb 198   = wceq 1653  Rel wrel 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781  df-rel 5317

This theorem is referenced by:  reliun  5441  reluni  5443  relint  5444  reldmmpt2  7003  wfrrel  7657  tfrlem6  7715  relsdom  8200  cda1dif  9284  0rest  16401  firest  16404  2oppchomf  16694  oppchofcl  17211  oyoncl  17221  releqg  17950  reldvdsr  18956  restbas  21287  hlimcaui  28609  frrlem6  32293  relbigcup  32508  fnsingle  32530  funimage  32539  colinrel  32668  cnfinltrel  33730  brcnvrabga  34595  relcoels  34664  neicvgnvor  39183  xlimrel  40777