Theorem releqi 5762

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  Rel wrel 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-rel 5665

This theorem is used by:  reluni  5805  relint  5806  relres  6012  reldmmpo  7584  frrlem6  8347  tfrlem6OLD  8428  relsdom  9018  0rest  17650  firest  17653  2oppchomf  17948  oppchofcl  18484  oyoncl  18494  releqg  19435  reldvdsr  20641  restbas  23531  hlimcaui  31895  gonan0  36365  satffunlem2lem2  36379  relbigcup  36874  fnsingle  36896  funimage  36905  colinrel  37037  brcnvrabga  39540  relqmap  39650  relcoels  39712  iscard4  44795  neicvgnvor  45377  relpropg  46182  grpcanonhfstruct  46299  xlimrel  47103  tposideq2  50333  reldmxpc  50699  reldmprcof1  50847  reldmlmd2  51167  reldmcmd2  51168  rellmd  51173  relcmd  51174