Theorem releqd 5343

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1630  Rel wrel 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-in 3728  df-ss 3735  df-rel 5256

This theorem is referenced by:  dftpos3  7521  tposfo2  7526  tposf12  7528  relexp0rel  13984  relexprelg  13985  relexpaddg  14000  imasaddfnlem  16395  imasvscafn  16404  cicer  16672  joindmss  17214  meetdmss  17228  mattpostpos  20477  cnextrel  22086  perpln1  25825  perpln2  25826  relfae  30644  cnfinltrel  33571  dibvalrel  36966  dicvalrelN  36988  diclspsn  36997  dihvalrel  37082  dih1  37089  dihmeetlem4preN  37109