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 206   = wceq 1540  Rel wrel 5624

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920  df-rel 5626

This theorem is referenced by:  dftpos3  8177  tposfo2  8182  tposf12  8184  relexp0rel  14944  relexprelg  14945  relexpreld  14947  relexpaddg  14960  imasaddfnlem  17432  imasvscafn  17441  cicer  17713  joindmss  18283  meetdmss  18297  mattpostpos  22339  cnextrel  23948  perpln1  28655  perpln2  28656  erler  33205  opprabs  33419  relfae  34214  satfrel  35340  dibvalrel  41142  dicvalrelN  41164  diclspsn  41173  dihvalrel  41258  dih1  41265  dihmeetlem4preN  41285  relcic  49030  oppfvalg  49111  oppfvallem  49120  funcoppc3  49132  uptposlem  49182  reldmprcof1  49366  reldmprcof2  49367  reldmlan2  49602  reldmran2  49603  rellan  49608  relran  49609