Theorem releqi 5735

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

Syntax hints:   ↔ wb 206   = wceq 1542  Rel wrel 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-rel 5639

This theorem is referenced by:  reluni  5775  relint  5776  reldmmpo  7502  frrlem6  8243  tfrlem6  8323  relsdom  8902  0rest  17361  firest  17364  2oppchomf  17659  oppchofcl  18195  oyoncl  18205  releqg  19116  reldvdsr  20308  restbas  23114  hlimcaui  31324  gonan0  35608  satffunlem2lem2  35622  relbigcup  36111  fnsingle  36133  funimage  36142  colinrel  36273  brcnvrabga  38593  relqmap  38703  relcoels  38765  iscard4  43889  neicvgnvor  44472  xlimrel  46178  tposideq2  49248  reldmxpc  49605  reldmprcof1  49740  reldmlmd2  50012  reldmcmd2  50013  rellmd  50018  relcmd  50019