Theorem releqd 5767

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  Rel wrel 5668

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-rel 5670

This theorem is used by:  dftpos3  8246  tposfo2  8251  tposf12  8253  relexp0rel  15100  relexprelg  15101  relexpreld  15103  relexpaddg  15116  imasaddfnlem  17606  imasvscafn  17615  cicer  17887  joindmss  18457  meetdmss  18471  mattpostpos  22663  cnextrel  24273  perpln1  29043  perpln2  29044  erler  33651  opprabs  33830  relfae  34704  satfrel  35898  relecxrn  39116  dibvalrel  41997  dicvalrelN  42019  diclspsn  42028  dihvalrel  42113  dih1  42120  dihmeetlem4preN  42140  relcic  49882  oppfvalg  49963  oppfvallem  49972  funcoppc3  49984  uptposlem  50034  reldmprcof1  50218  reldmprcof2  50219  reldmlan2  50454  reldmran2  50455  rellan  50460  relran  50461