MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  releqd Structured version   Visualization version   GIF version

Theorem releqd 5111
Description: Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
Hypothesis
Ref Expression
releqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
releqd (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))

Proof of Theorem releqd
StepHypRef Expression
1 releqd.1 . 2 (𝜑𝐴 = 𝐵)
2 releq 5109 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2syl 17 1 (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  Rel wrel 5028
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2591  df-cleq 2597  df-clel 2600  df-in 3541  df-ss 3548  df-rel 5030
This theorem is referenced by:  dftpos3  7229  tposfo2  7234  tposf12  7236  relexp0rel  13566  relexprelg  13567  relexpaddg  13582  imasaddfnlem  15952  imasvscafn  15961  cicer  16230  joindmss  16771  meetdmss  16785  mattpostpos  20016  cnextrel  21614  perpln1  25318  perpln2  25319  relfae  29438  dibvalrel  35268  dicvalrelN  35290  diclspsn  35299  dihvalrel  35384  dih1  35391  dihmeetlem4preN  35411
  Copyright terms: Public domain W3C validator