Theorem releqd 5729

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907  df-rel 5632

This theorem is referenced by:  dftpos3  8188  tposfo2  8193  tposf12  8195  relexp0rel  14993  relexprelg  14994  relexpreld  14996  relexpaddg  15009  imasaddfnlem  17486  imasvscafn  17495  cicer  17767  joindmss  18337  meetdmss  18351  mattpostpos  22432  cnextrel  24041  perpln1  28795  perpln2  28796  erler  33344  opprabs  33560  relfae  34410  satfrel  35568  relecxrn  38745  dibvalrel  41626  dicvalrelN  41648  diclspsn  41657  dihvalrel  41742  dih1  41749  dihmeetlem4preN  41769  relcic  49535  oppfvalg  49616  oppfvallem  49625  funcoppc3  49637  uptposlem  49687  reldmprcof1  49871  reldmprcof2  49872  reldmlan2  50107  reldmran2  50108  rellan  50113  relran  50114