Theorem releqd 5728

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  Rel wrel 5629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918  df-rel 5631

This theorem is referenced by:  dftpos3  8186  tposfo2  8191  tposf12  8193  relexp0rel  14960  relexprelg  14961  relexpreld  14963  relexpaddg  14976  imasaddfnlem  17449  imasvscafn  17458  cicer  17730  joindmss  18300  meetdmss  18314  mattpostpos  22398  cnextrel  24007  perpln1  28782  perpln2  28783  erler  33347  opprabs  33563  relfae  34404  satfrel  35561  relecxrn  38592  dibvalrel  41423  dicvalrelN  41445  diclspsn  41454  dihvalrel  41539  dih1  41546  dihmeetlem4preN  41566  relcic  49290  oppfvalg  49371  oppfvallem  49380  funcoppc3  49392  uptposlem  49442  reldmprcof1  49626  reldmprcof2  49627  reldmlan2  49862  reldmran2  49863  rellan  49868  relran  49869