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

Theorem releqi 4923
Description: Equality inference for the relation predicate. (Contributed by NM, 8-Dec-2006.)
Hypothesis
Ref Expression
releqi.1  |-  A  =  B
Assertion
Ref Expression
releqi  |-  ( Rel 
A  <->  Rel  B )

Proof of Theorem releqi
StepHypRef Expression
1 releqi.1 . 2  |-  A  =  B
2 releq 4922 . 2  |-  ( A  =  B  ->  ( Rel  A  <->  Rel  B ) )
31, 2ax-mp 5 1  |-  ( Rel 
A  <->  Rel  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    = wceq 1452   Rel wrel 4844
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-in 3397  df-ss 3404  df-rel 4846
This theorem is referenced by:  reliun  4959  reluni  4961  relint  4962  reldmmpt2  6426  wfrrel  7059  tfrlem6  7118  relsdom  7594  cda1dif  8624  0rest  15406  firest  15409  2oppchomf  15707  oppchofcl  16223  oyoncl  16233  releqg  16942  reldvdsr  17950  restbas  20251  hlimcaui  26970  relbigcup  30735  fnsingle  30757  funimage  30766  colinrel  30895
  Copyright terms: Public domain W3C validator