Theorem releqd 5689

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  Rel wrel 5594

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-rel 5596

This theorem is referenced by:  dftpos3  8060  tposfo2  8065  tposf12  8067  relexp0rel  14748  relexprelg  14749  relexpreld  14751  relexpaddg  14764  imasaddfnlem  17239  imasvscafn  17248  cicer  17518  joindmss  18097  meetdmss  18111  mattpostpos  21603  cnextrel  23214  perpln1  27071  perpln2  27072  relfae  32215  satfrel  33329  dibvalrel  39177  dicvalrelN  39199  diclspsn  39208  dihvalrel  39293  dih1  39300  dihmeetlem4preN  39320