Theorem releqd 5756

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  Rel wrel 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897  df-rel 5658

This theorem is used by:  dftpos3  8269  tposfo2  8274  tposf12  8276  relexp0rel  15199  relexprelg  15200  relexpreld  15202  relexpaddg  15215  imasaddfnlem  17709  imasvscafn  17718  cicer  17990  joindmss  18560  meetdmss  18574  mattpostpos  22778  cnextrel  24391  perpln1  29194  perpln2  29195  erler  33876  opprabs  34056  relfae  34930  satfrel  36250  relecxrn  39476  dibvalrel  42357  dicvalrelN  42379  diclspsn  42388  dihvalrel  42473  dih1  42480  dihmeetlem4preN  42500  relcic  50295  oppfvalg  50378  oppfvallem  50387  funcoppc3  50399  uptposlem  50449  reldmprcof1  50652  reldmprcof2  50653  reldmlan2  50936  reldmran2  50937  rellan  50942  relran  50943