Theorem releqi 5764

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

Syntax hints:   ↔ wb 209   = wceq 1570  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922  df-rel 5668

This theorem is referenced by:  reluni  5805  relint  5806  reldmmpo  7544  frrlem6  8284  tfrlem6OLD  8365  relsdom  8946  0rest  17477  firest  17480  2oppchomf  17775  oppchofcl  18311  oyoncl  18321  releqg  19236  reldvdsr  20438  restbas  23315  hlimcaui  31588  gonan0  35884  satffunlem2lem2  35898  relbigcup  36387  fnsingle  36409  funimage  36418  colinrel  36549  brcnvrabga  39011  relqmap  39121  relcoels  39183  iscard4  44279  neicvgnvor  44862  xlimrel  46554  tposideq2  49687  reldmxpc  50044  reldmprcof1  50179  reldmlmd2  50451  reldmcmd2  50452  rellmd  50457  relcmd  50458