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

Theorem releq 4771
Description: Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
releq  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )

Proof of Theorem releq
StepHypRef Expression
1 sseq1 3199 . 2  |-  ( A  =  B  ->  ( A  C_  ( _V  X.  _V )  <->  B  C_  ( _V 
X.  _V ) ) )
2 df-rel 4696 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
3 df-rel 4696 . 2  |-  ( Rel 
B  <->  B  C_  ( _V 
X.  _V ) )
41, 2, 33bitr4g 279 1  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   _Vcvv 2788    C_ wss 3152    X. cxp 4687   Rel wrel 4694
This theorem is referenced by:  releqi  4772  releqd  4773  dfrel2  5124  tposfn2  6256  ereq1  6667  isps  14311  isdir  14354  relexprel  24031  wfrlem6  24261  frrlem6  24290  cur1vald  25199  valcurfn1  25204  isprsr  25224  prtlem12  26735  bnj1321  29057
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166  df-rel 4696
  Copyright terms: Public domain W3C validator