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

Theorem releqd 5343
 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 5341 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2syl 17 1 (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630  Rel wrel 5254 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-in 3728  df-ss 3735  df-rel 5256 This theorem is referenced by:  dftpos3  7521  tposfo2  7526  tposf12  7528  relexp0rel  13984  relexprelg  13985  relexpaddg  14000  imasaddfnlem  16395  imasvscafn  16404  cicer  16672  joindmss  17214  meetdmss  17228  mattpostpos  20477  cnextrel  22086  perpln1  25825  perpln2  25826  relfae  30644  cnfinltrel  33571  dibvalrel  36966  dicvalrelN  36988  diclspsn  36997  dihvalrel  37082  dih1  37089  dihmeetlem4preN  37109
 Copyright terms: Public domain W3C validator