Theorem releqd 5765

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  Rel wrel 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922  df-rel 5668

This theorem is referenced by:  dftpos3  8236  tposfo2  8241  tposf12  8243  relexp0rel  15070  relexprelg  15071  relexpreld  15073  relexpaddg  15086  imasaddfnlem  17577  imasvscafn  17586  cicer  17858  joindmss  18428  meetdmss  18442  mattpostpos  22611  cnextrel  24220  perpln1  28990  perpln2  28991  erler  33585  opprabs  33764  relfae  34637  satfrel  35859  relecxrn  39056  dibvalrel  41937  dicvalrelN  41959  diclspsn  41968  dihvalrel  42053  dih1  42060  dihmeetlem4preN  42080  relcic  49823  oppfvalg  49904  oppfvallem  49913  funcoppc3  49925  uptposlem  49975  reldmprcof1  50159  reldmprcof2  50160  reldmlan2  50395  reldmran2  50396  rellan  50401  relran  50402