Theorem releqd 5724

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  Rel wrel 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-ss 3901  df-rel 5627

This theorem is referenced by:  dftpos3  8186  tposfo2  8191  tposf12  8193  relexp0rel  14994  relexprelg  14995  relexpreld  14997  relexpaddg  15010  imasaddfnlem  17487  imasvscafn  17496  cicer  17768  joindmss  18338  meetdmss  18352  mattpostpos  22440  cnextrel  24049  perpln1  28798  perpln2  28799  erler  33348  opprabs  33567  relfae  34441  satfrel  35608  relecxrn  38787  dibvalrel  41668  dicvalrelN  41690  diclspsn  41699  dihvalrel  41784  dih1  41791  dihmeetlem4preN  41811  relcic  49547  oppfvalg  49628  oppfvallem  49637  funcoppc3  49649  uptposlem  49699  reldmprcof1  49883  reldmprcof2  49884  reldmlan2  50119  reldmran2  50120  rellan  50125  relran  50126