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

Theorem releqd 5193
Description: Equality deduction for the relation predicate. (Contributed by NM, 8-Mar-2014.)
Hypothesis
Ref Expression
releqd.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
releqd (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))

Proof of Theorem releqd
StepHypRef Expression
1 releqd.1 . 2 (𝜑𝐴 = 𝐵)
2 releq 5191 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2syl 17 1 (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  Rel wrel 5109
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581  df-rel 5111
This theorem is referenced by:  dftpos3  7355  tposfo2  7360  tposf12  7362  relexp0rel  13758  relexprelg  13759  relexpaddg  13774  imasaddfnlem  16169  imasvscafn  16178  cicer  16447  joindmss  16988  meetdmss  17002  mattpostpos  20241  cnextrel  21848  perpln1  25586  perpln2  25587  relfae  30284  dibvalrel  36271  dicvalrelN  36293  diclspsn  36302  dihvalrel  36387  dih1  36394  dihmeetlem4preN  36414
  Copyright terms: Public domain W3C validator