Theorem releqd 5733

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  Rel wrel 5636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928  df-rel 5638

This theorem is referenced by:  dftpos3  8200  tposfo2  8205  tposf12  8207  relexp0rel  14979  relexprelg  14980  relexpreld  14982  relexpaddg  14995  imasaddfnlem  17467  imasvscafn  17476  cicer  17744  joindmss  18314  meetdmss  18328  mattpostpos  22317  cnextrel  23926  perpln1  28613  perpln2  28614  erler  33189  opprabs  33426  relfae  34210  satfrel  35327  dibvalrel  41130  dicvalrelN  41152  diclspsn  41161  dihvalrel  41246  dih1  41253  dihmeetlem4preN  41273  relcic  49007  oppfvalg  49088  oppfvallem  49097  funcoppc3  49109  uptposlem  49159  reldmprcof1  49343  reldmprcof2  49344  reldmlan2  49579  reldmran2  49580  rellan  49585  relran  49586