Theorem releqd 5776

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  Rel wrel 5680

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-rel 5682

This theorem is referenced by:  dftpos3  8225  tposfo2  8230  tposf12  8232  relexp0rel  14980  relexprelg  14981  relexpreld  14983  relexpaddg  14996  imasaddfnlem  17470  imasvscafn  17479  cicer  17749  joindmss  18328  meetdmss  18342  mattpostpos  21947  cnextrel  23558  perpln1  27950  perpln2  27951  opprabs  32584  relfae  33233  satfrel  34346  dibvalrel  40022  dicvalrelN  40044  diclspsn  40053  dihvalrel  40138  dih1  40145  dihmeetlem4preN  40165