Theorem releqd 5766

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  Rel wrel 5667

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930  df-rel 5669

This theorem is referenced by:  dftpos3  8239  tposfo2  8244  tposf12  8246  relexp0rel  15073  relexprelg  15074  relexpreld  15076  relexpaddg  15089  imasaddfnlem  17581  imasvscafn  17590  cicer  17862  joindmss  18432  meetdmss  18446  mattpostpos  22579  cnextrel  24188  perpln1  28948  perpln2  28949  erler  33525  opprabs  33708  relfae  34581  satfrel  35757  relecxrn  38945  dibvalrel  41826  dicvalrelN  41848  diclspsn  41857  dihvalrel  41942  dih1  41949  dihmeetlem4preN  41969  relcic  49707  oppfvalg  49788  oppfvallem  49797  funcoppc3  49809  uptposlem  49859  reldmprcof1  50043  reldmprcof2  50044  reldmlan2  50279  reldmran2  50280  rellan  50285  relran  50286