Theorem releqd 5779

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  Rel wrel 5682

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-rel 5684

This theorem is referenced by:  dftpos3  8229  tposfo2  8234  tposf12  8236  relexp0rel  14984  relexprelg  14985  relexpreld  14987  relexpaddg  15000  imasaddfnlem  17474  imasvscafn  17483  cicer  17753  joindmss  18332  meetdmss  18346  mattpostpos  21956  cnextrel  23567  perpln1  27992  perpln2  27993  opprabs  32627  relfae  33276  satfrel  34389  dibvalrel  40082  dicvalrelN  40104  diclspsn  40113  dihvalrel  40198  dih1  40205  dihmeetlem4preN  40225