Theorem releqi 5734

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-rel 5638

This theorem is referenced by:  reluni  5774  relint  5775  reldmmpo  7501  frrlem6  8241  tfrlem6  8321  relsdom  8900  0rest  17392  firest  17395  2oppchomf  17690  oppchofcl  18226  oyoncl  18236  releqg  19150  reldvdsr  20340  restbas  23123  hlimcaui  31307  gonan0  35574  satffunlem2lem2  35588  relbigcup  36077  fnsingle  36099  funimage  36108  colinrel  36239  brcnvrabga  38663  relqmap  38773  relcoels  38835  iscard4  43960  neicvgnvor  44543  xlimrel  46248  tposideq2  49364  reldmxpc  49721  reldmprcof1  49856  reldmlmd2  50128  reldmcmd2  50129  rellmd  50134  relcmd  50135