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

Theorem releqd 5630
 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 5628 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2syl 17 1 (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  Rel wrel 5537 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-v 3471  df-in 3915  df-ss 3925  df-rel 5539 This theorem is referenced by:  dftpos3  7897  tposfo2  7902  tposf12  7904  relexp0rel  14387  relexprelg  14388  relexpaddg  14403  imasaddfnlem  16792  imasvscafn  16801  cicer  17067  joindmss  17608  meetdmss  17622  mattpostpos  21057  cnextrel  22666  perpln1  26502  perpln2  26503  relfae  31580  satfrel  32688  dibvalrel  38417  dicvalrelN  38439  diclspsn  38448  dihvalrel  38533  dih1  38540  dihmeetlem4preN  38560
 Copyright terms: Public domain W3C validator