Theorem releqi 5732

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

Syntax hints:   ↔ wb 206   = wceq 1540  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-rel 5638

This theorem is referenced by:  reliun  5770  reluni  5772  relint  5773  reldmmpo  7503  frrlem6  8247  tfrlem6  8327  relsdom  8902  0rest  17368  firest  17371  2oppchomf  17665  oppchofcl  18201  oyoncl  18211  releqg  19089  reldvdsr  20280  restbas  23078  hlimcaui  31215  gonan0  35372  satffunlem2lem2  35386  relbigcup  35878  fnsingle  35900  funimage  35909  colinrel  36038  brcnvrabga  38317  relcoels  38408  iscard4  43515  neicvgnvor  44098  xlimrel  45811  tposideq2  48870  reldmxpc  49228  reldmprcof1  49363  reldmlmd2  49635  reldmcmd2  49636  rellmd  49641  relcmd  49642