Theorem releqd 5788

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968  df-rel 5692

This theorem is referenced by:  dftpos3  8269  tposfo2  8274  tposf12  8276  relexp0rel  15076  relexprelg  15077  relexpreld  15079  relexpaddg  15092  imasaddfnlem  17573  imasvscafn  17582  cicer  17850  joindmss  18424  meetdmss  18438  mattpostpos  22460  cnextrel  24071  perpln1  28718  perpln2  28719  erler  33269  opprabs  33510  relfae  34248  satfrel  35372  dibvalrel  41165  dicvalrelN  41187  diclspsn  41196  dihvalrel  41281  dih1  41288  dihmeetlem4preN  41308