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

Theorem releq 5406
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 3822 . 2 (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V)))
2 df-rel 5319 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3 df-rel 5319 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
41, 2, 33bitr4g 306 1 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1653  Vcvv 3385  wss 3769   × cxp 5310  Rel wrel 5317
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-in 3776  df-ss 3783  df-rel 5319
This theorem is referenced by:  releqi  5407  releqd  5408  dfrel2  5800  tposfn2  7612  ereq1  7989  isps  17517  isdir  17547  fpwrelmapffslem  30025  bnj1321  31612  cnfinltrel  33739  refreleq  34764  symreleq  34798  trreleq  34822  prtlem12  34888  relintabex  38666  clrellem  38708  clcnvlem  38709
  Copyright terms: Public domain W3C validator