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

Theorem releqd 5739
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 5737 . 2 (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
31, 2syl 17 1 (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  Rel wrel 5643
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-rel 5645
This theorem is referenced by:  dftpos3  8180  tposfo2  8185  tposf12  8187  relexp0rel  14929  relexprelg  14930  relexpreld  14932  relexpaddg  14945  imasaddfnlem  17417  imasvscafn  17426  cicer  17696  joindmss  18275  meetdmss  18289  mattpostpos  21819  cnextrel  23430  perpln1  27694  perpln2  27695  relfae  32886  satfrel  34001  dibvalrel  39655  dicvalrelN  39677  diclspsn  39686  dihvalrel  39771  dih1  39778  dihmeetlem4preN  39798
  Copyright terms: Public domain W3C validator