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

Theorem releq 5782
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 4005 . 2 (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V)))
2 df-rel 5689 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3 df-rel 5689 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
41, 2, 33bitr4g 313 1 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1534  Vcvv 3462  wss 3947   × cxp 5680  Rel wrel 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3964  df-rel 5689
This theorem is referenced by:  releqi  5783  releqd  5784  relsnb  5808  dfrel2  6200  tposfn2  8263  ereq1  8741  isps  18593  isdir  18623  fpwrelmapffslem  32646  bnj1321  34872  refreleq  38219  symreleq  38256  trreleq  38280  prtlem12  38565  relintabex  43248  clrellem  43289  clcnvlem  43290
  Copyright terms: Public domain W3C validator