Theorem releqi 5767

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

Syntax hints:   ↔ wb 206   = wceq 1539  Rel wrel 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948  df-rel 5672

This theorem is referenced by:  reliun  5806  reluni  5808  relint  5809  reldmmpo  7549  frrlem6  8298  wfrrelOLD  8336  tfrlem6  8404  relsdom  8974  0rest  17445  firest  17448  2oppchomf  17738  oppchofcl  18275  oyoncl  18285  releqg  19162  reldvdsr  20328  restbas  23112  hlimcaui  31183  gonan0  35356  satffunlem2lem2  35370  relbigcup  35857  fnsingle  35879  funimage  35888  colinrel  36017  brcnvrabga  38302  relcoels  38384  iscard4  43508  neicvgnvor  44091  xlimrel  45792  tposideq2  48748  reldmxpc  48923