Theorem releqd 5802

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993  df-rel 5707

This theorem is referenced by:  dftpos3  8285  tposfo2  8290  tposf12  8292  relexp0rel  15086  relexprelg  15087  relexpreld  15089  relexpaddg  15102  imasaddfnlem  17588  imasvscafn  17597  cicer  17867  joindmss  18449  meetdmss  18463  mattpostpos  22481  cnextrel  24092  perpln1  28736  perpln2  28737  erler  33237  opprabs  33475  relfae  34211  satfrel  35335  dibvalrel  41120  dicvalrelN  41142  diclspsn  41151  dihvalrel  41236  dih1  41243  dihmeetlem4preN  41263