Theorem releqd 5726

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

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

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916  df-rel 5629

This theorem is referenced by:  dftpos3  8184  tposfo2  8189  tposf12  8191  relexp0rel  14958  relexprelg  14959  relexpreld  14961  relexpaddg  14974  imasaddfnlem  17447  imasvscafn  17456  cicer  17728  joindmss  18298  meetdmss  18312  mattpostpos  22396  cnextrel  24005  perpln1  28731  perpln2  28732  erler  33296  opprabs  33512  relfae  34353  satfrel  35510  relecxrn  38531  dibvalrel  41362  dicvalrelN  41384  diclspsn  41393  dihvalrel  41478  dih1  41485  dihmeetlem4preN  41505  relcic  49232  oppfvalg  49313  oppfvallem  49322  funcoppc3  49334  uptposlem  49384  reldmprcof1  49568  reldmprcof2  49569  reldmlan2  49804  reldmran2  49805  rellan  49810  relran  49811