Theorem releqd 5744

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  Rel wrel 5646

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934  df-rel 5648

This theorem is referenced by:  dftpos3  8226  tposfo2  8231  tposf12  8233  relexp0rel  15010  relexprelg  15011  relexpreld  15013  relexpaddg  15026  imasaddfnlem  17498  imasvscafn  17507  cicer  17775  joindmss  18345  meetdmss  18359  mattpostpos  22348  cnextrel  23957  perpln1  28644  perpln2  28645  erler  33223  opprabs  33460  relfae  34244  satfrel  35361  dibvalrel  41164  dicvalrelN  41186  diclspsn  41195  dihvalrel  41280  dih1  41287  dihmeetlem4preN  41307  relcic  49038  oppfvalg  49119  oppfvallem  49128  funcoppc3  49140  uptposlem  49190  reldmprcof1  49374  reldmprcof2  49375  reldmlan2  49610  reldmran2  49611  rellan  49616  relran  49617