Theorem releqd 5790

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 5788	. 2 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (Rel 𝐴 ↔ Rel 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  Rel wrel 5693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979  df-rel 5695

This theorem is referenced by:  dftpos3  8267  tposfo2  8272  tposf12  8274  relexp0rel  15072  relexprelg  15073  relexpreld  15075  relexpaddg  15088  imasaddfnlem  17574  imasvscafn  17583  cicer  17853  joindmss  18436  meetdmss  18450  mattpostpos  22475  cnextrel  24086  perpln1  28732  perpln2  28733  erler  33251  opprabs  33489  relfae  34227  satfrel  35351  dibvalrel  41145  dicvalrelN  41167  diclspsn  41176  dihvalrel  41261  dih1  41268  dihmeetlem4preN  41288