Theorem releqi 5721

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

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

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 3920  df-rel 5626

This theorem is referenced by:  reliun  5759  reluni  5761  relint  5762  reldmmpo  7483  frrlem6  8224  tfrlem6  8304  relsdom  8879  0rest  17333  firest  17336  2oppchomf  17630  oppchofcl  18166  oyoncl  18176  releqg  19054  reldvdsr  20245  restbas  23043  hlimcaui  31180  gonan0  35369  satffunlem2lem2  35383  relbigcup  35875  fnsingle  35897  funimage  35906  colinrel  36035  brcnvrabga  38314  relcoels  38405  iscard4  43510  neicvgnvor  44093  xlimrel  45805  tposideq2  48877  reldmxpc  49235  reldmprcof1  49370  reldmlmd2  49642  reldmcmd2  49643  rellmd  49648  relcmd  49649