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

Theorem releqd 5077
Description: Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
Hypothesis
Ref Expression
releqd.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
releqd  |-  ( ph  ->  ( Rel  A  <->  Rel  B ) )

Proof of Theorem releqd
StepHypRef Expression
1 releqd.1 . 2  |-  ( ph  ->  A  =  B )
2 releq 5075 . 2  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( Rel  A  <->  Rel  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383   Rel wrel 4994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-rel 4996
This theorem is referenced by:  dftpos3  6975  tposfo2  6980  tposf12  6982  imasaddfnlem  14906  imasvscafn  14915  joindmss  15615  meetdmss  15629  mattpostpos  18933  cnextrel  20540  perpln1  24063  perpln2  24064  relfae  28196  dibvalrel  36630  dicvalrelN  36652  diclspsn  36661  dihvalrel  36746  dih1  36753  dihmeetlem4preN  36773
  Copyright terms: Public domain W3C validator