Theorem releqd 5691

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

Step	Hyp	Ref	Expression
1		releqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		releq 5689	. 2 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  Rel wrel 5596

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3433  df-in 3895  df-ss 3905  df-rel 5598

This theorem is referenced by:  dftpos3  8058  tposfo2  8063  tposf12  8065  relexp0rel  14746  relexprelg  14747  relexpreld  14749  relexpaddg  14762  imasaddfnlem  17237  imasvscafn  17246  cicer  17516  joindmss  18095  meetdmss  18109  mattpostpos  21601  cnextrel  23212  perpln1  27069  perpln2  27070  relfae  32212  satfrel  33326  dibvalrel  39174  dicvalrelN  39196  diclspsn  39205  dihvalrel  39290  dih1  39297  dihmeetlem4preN  39317