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

Theorem releq 4874
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 3285 . 2  |-  ( A  =  B  ->  ( A  C_  ( _V  X.  _V )  <->  B  C_  ( _V 
X.  _V ) ) )
2 df-rel 4799 . 2  |-  ( Rel 
A  <->  A  C_  ( _V 
X.  _V ) )
3 df-rel 4799 . 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 1647   _Vcvv 2873    C_ wss 3238    X. cxp 4790   Rel wrel 4797
This theorem is referenced by:  releqi  4875  releqd  4876  dfrel2  5227  tposfn2  6398  ereq1  6809  isps  14521  isdir  14564  relfae  24182  relexprel  24703  wfrlem6  25087  frrlem6  25116  prtlem12  26326  bnj1321  28809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252  df-rel 4799
  Copyright terms: Public domain W3C validator