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

Theorem releqd 5080
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 5078 . 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 1374   Rel wrel 4999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3478  df-ss 3485  df-rel 5001
This theorem is referenced by:  dftpos3  6965  tposfo2  6970  tposf12  6972  imasaddfnlem  14774  imasvscafn  14783  joindmss  15485  meetdmss  15499  mattpostpos  18718  cnextrel  20293  perpln1  23790  perpln2  23791  relfae  27847  dibvalrel  35837  dicvalrelN  35859  diclspsn  35868  dihvalrel  35953  dih1  35960  dihmeetlem4preN  35980
  Copyright terms: Public domain W3C validator