Theorem releqd 5722

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  Rel wrel 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900  df-rel 5625

This theorem is referenced by:  dftpos3  8184  tposfo2  8189  tposf12  8191  relexp0rel  14990  relexprelg  14991  relexpreld  14993  relexpaddg  15006  imasaddfnlem  17483  imasvscafn  17492  cicer  17764  joindmss  18334  meetdmss  18348  mattpostpos  22437  cnextrel  24046  perpln1  28796  perpln2  28797  erler  33346  opprabs  33565  relfae  34431  satfrel  35595  relecxrn  38774  dibvalrel  41655  dicvalrelN  41677  diclspsn  41686  dihvalrel  41771  dih1  41778  dihmeetlem4preN  41798  relcic  49535  oppfvalg  49616  oppfvallem  49625  funcoppc3  49637  uptposlem  49687  reldmprcof1  49871  reldmprcof2  49872  reldmlan2  50107  reldmran2  50108  rellan  50113  relran  50114