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

Theorem releqd 5788
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 5786 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2syl 17 1 (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  Rel wrel 5690
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-rel 5692
This theorem is referenced by:  dftpos3  8269  tposfo2  8274  tposf12  8276  relexp0rel  15076  relexprelg  15077  relexpreld  15079  relexpaddg  15092  imasaddfnlem  17573  imasvscafn  17582  cicer  17850  joindmss  18424  meetdmss  18438  mattpostpos  22460  cnextrel  24071  perpln1  28718  perpln2  28719  erler  33269  opprabs  33510  relfae  34248  satfrel  35372  dibvalrel  41165  dicvalrelN  41187  diclspsn  41196  dihvalrel  41281  dih1  41288  dihmeetlem4preN  41308
  Copyright terms: Public domain W3C validator