Theorem releqd 5617

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  Rel wrel 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-rel 5526

This theorem is referenced by:  dftpos3  7893  tposfo2  7898  tposf12  7900  relexp0rel  14388  relexprelg  14389  relexpreld  14391  relexpaddg  14404  imasaddfnlem  16793  imasvscafn  16802  cicer  17068  joindmss  17609  meetdmss  17623  mattpostpos  21059  cnextrel  22668  perpln1  26504  perpln2  26505  relfae  31616  satfrel  32727  dibvalrel  38459  dicvalrelN  38481  diclspsn  38490  dihvalrel  38575  dih1  38582  dihmeetlem4preN  38602