Theorem releqd 5751

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  Rel wrel 5652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921  df-rel 5654

This theorem is referenced by:  dftpos3  8224  tposfo2  8229  tposf12  8231  relexp0rel  15050  relexprelg  15051  relexpreld  15053  relexpaddg  15066  imasaddfnlem  17558  imasvscafn  17567  cicer  17839  joindmss  18409  meetdmss  18423  mattpostpos  22514  cnextrel  24123  perpln1  28883  perpln2  28884  erler  33446  opprabs  33670  relfae  34544  satfrel  35717  relecxrn  38906  dibvalrel  41787  dicvalrelN  41809  diclspsn  41818  dihvalrel  41903  dih1  41910  dihmeetlem4preN  41930  relcic  49666  oppfvalg  49747  oppfvallem  49756  funcoppc3  49768  uptposlem  49818  reldmprcof1  50002  reldmprcof2  50003  reldmlan2  50238  reldmran2  50239  rellan  50244  relran  50245