Theorem releqi 5755

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897  df-rel 5658

This theorem is used by:  reluni  5797  relint  5798  relres  5997  reldmmpo  7558  frrlem6  8317  tfrlem6OLD  8398  relsdom  8988  0rest  17609  firest  17612  2oppchomf  17907  oppchofcl  18443  oyoncl  18453  releqg  19394  reldvdsr  20599  restbas  23485  hlimcaui  31847  gonan0  36275  satffunlem2lem2  36289  relbigcup  36783  fnsingle  36805  funimage  36814  colinrel  36946  brcnvrabga  39411  relqmap  39521  relcoels  39583  iscard4  44671  neicvgnvor  45253  xlimrel  46966  tposideq2  50138  reldmxpc  50504  reldmprcof1  50652  reldmlmd2  50972  reldmcmd2  50973  rellmd  50978  relcmd  50979