Theorem releqd 5735

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-rel 5638

This theorem is referenced by:  dftpos3  8194  tposfo2  8199  tposf12  8201  relexp0rel  14999  relexprelg  15000  relexpreld  15002  relexpaddg  15015  imasaddfnlem  17492  imasvscafn  17501  cicer  17773  joindmss  18343  meetdmss  18357  mattpostpos  22419  cnextrel  24028  perpln1  28778  perpln2  28779  erler  33326  opprabs  33542  relfae  34391  satfrel  35549  relecxrn  38728  dibvalrel  41609  dicvalrelN  41631  diclspsn  41640  dihvalrel  41725  dih1  41732  dihmeetlem4preN  41752  relcic  49520  oppfvalg  49601  oppfvallem  49610  funcoppc3  49622  uptposlem  49672  reldmprcof1  49856  reldmprcof2  49857  reldmlan2  50092  reldmran2  50093  rellan  50098  relran  50099