Theorem releqd 5718

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  Rel wrel 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914  df-rel 5621

This theorem is referenced by:  dftpos3  8174  tposfo2  8179  tposf12  8181  relexp0rel  14944  relexprelg  14945  relexpreld  14947  relexpaddg  14960  imasaddfnlem  17432  imasvscafn  17441  cicer  17713  joindmss  18283  meetdmss  18297  mattpostpos  22369  cnextrel  23978  perpln1  28688  perpln2  28689  erler  33232  opprabs  33447  relfae  34260  satfrel  35411  dibvalrel  41210  dicvalrelN  41232  diclspsn  41241  dihvalrel  41326  dih1  41333  dihmeetlem4preN  41353  relcic  49085  oppfvalg  49166  oppfvallem  49175  funcoppc3  49187  uptposlem  49237  reldmprcof1  49421  reldmprcof2  49422  reldmlan2  49657  reldmran2  49658  rellan  49663  relran  49664