Theorem releqd 5757

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  Rel wrel 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943  df-rel 5661

This theorem is referenced by:  dftpos3  8243  tposfo2  8248  tposf12  8250  relexp0rel  15056  relexprelg  15057  relexpreld  15059  relexpaddg  15072  imasaddfnlem  17542  imasvscafn  17551  cicer  17819  joindmss  18389  meetdmss  18403  mattpostpos  22392  cnextrel  24001  perpln1  28689  perpln2  28690  erler  33260  opprabs  33497  relfae  34278  satfrel  35389  dibvalrel  41182  dicvalrelN  41204  diclspsn  41213  dihvalrel  41298  dih1  41305  dihmeetlem4preN  41325  relcic  49012  oppfvalg  49074  oppfvallem  49081  funcoppc3  49090  uptposlem  49130  reldmprcof1  49291  reldmprcof2  49292  reldmlan2  49492  reldmran2  49493  rellan  49498  relran  49499