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

Theorem releqd 4938
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 4936 . 2  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )
31, 2syl 17 1  |-  ( ph  ->  ( Rel  A  <->  Rel  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437   Rel wrel 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-rel 4860
This theorem is referenced by:  dftpos3  7003  tposfo2  7008  tposf12  7010  relexp0rel  13101  relexprelg  13102  relexpaddg  13117  imasaddfnlem  15434  imasvscafn  15443  cicer  15711  joindmss  16253  meetdmss  16267  mattpostpos  19478  cnextrel  21077  perpln1  24754  perpln2  24755  relfae  29079  dibvalrel  34701  dicvalrelN  34723  diclspsn  34732  dihvalrel  34817  dih1  34824  dihmeetlem4preN  34844
  Copyright terms: Public domain W3C validator