Theorem releqi 5754

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

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

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 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916  df-rel 5658

This theorem is used by:  reluni  5796  relint  5797  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  36157  satffunlem2lem2  36171  relbigcup  36659  fnsingle  36681  funimage  36690  colinrel  36822  brcnvrabga  39274  relqmap  39384  relcoels  39446  iscard4  44533  neicvgnvor  45115  xlimrel  46829  tposideq2  49996  reldmxpc  50353  reldmprcof1  50488  reldmlmd2  50760  reldmcmd2  50761  rellmd  50766  relcmd  50767