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

Theorem releq 5777
Description: Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
releq (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))

Proof of Theorem releq
StepHypRef Expression
1 sseq1 4008 . 2 (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V)))
2 df-rel 5684 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3 df-rel 5684 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
41, 2, 33bitr4g 314 1 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  Vcvv 3475  wss 3949   × cxp 5675  Rel wrel 5682
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-rel 5684
This theorem is referenced by:  releqi  5778  releqd  5779  relsnb  5803  dfrel2  6189  tposfn2  8233  ereq1  8710  isps  18521  isdir  18551  fpwrelmapffslem  31957  bnj1321  34038  refreleq  37391  symreleq  37428  trreleq  37452  prtlem12  37737  relintabex  42332  clrellem  42373  clcnvlem  42374
  Copyright terms: Public domain W3C validator