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

Theorem releq 5341
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 3775 . 2 (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V)))
2 df-rel 5256 . 2 (Rel 𝐴𝐴 ⊆ (V × V))
3 df-rel 5256 . 2 (Rel 𝐵𝐵 ⊆ (V × V))
41, 2, 33bitr4g 303 1 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  Vcvv 3351  wss 3723   × cxp 5247  Rel wrel 5254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737  df-rel 5256
This theorem is referenced by:  releqi  5342  releqd  5343  dfrel2  5724  tposfn2  7526  ereq1  7903  isps  17410  isdir  17440  fpwrelmapffslem  29847  bnj1321  31433  cnfinltrel  33578  refreleq  34612  symreleq  34646  prtlem12  34675  relintabex  38413  clrellem  38455  clcnvlem  38456
  Copyright terms: Public domain W3C validator