Theorem releqd 5203

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  Rel wrel 5119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-rel 5121

This theorem is referenced by:  dftpos3  7370  tposfo2  7375  tposf12  7377  relexp0rel  13777  relexprelg  13778  relexpaddg  13793  imasaddfnlem  16188  imasvscafn  16197  cicer  16466  joindmss  17007  meetdmss  17021  mattpostpos  20260  cnextrel  21867  perpln1  25605  perpln2  25606  relfae  30310  dibvalrel  36452  dicvalrelN  36474  diclspsn  36483  dihvalrel  36568  dih1  36575  dihmeetlem4preN  36595