Theorem releqd 5784

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  Rel wrel 5687

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3964  df-rel 5689

This theorem is referenced by:  dftpos3  8259  tposfo2  8264  tposf12  8266  relexp0rel  15042  relexprelg  15043  relexpreld  15045  relexpaddg  15058  imasaddfnlem  17543  imasvscafn  17552  cicer  17822  joindmss  18404  meetdmss  18418  mattpostpos  22447  cnextrel  24058  perpln1  28637  perpln2  28638  erler  33120  opprabs  33357  relfae  34080  satfrel  35195  dibvalrel  40862  dicvalrelN  40884  diclspsn  40893  dihvalrel  40978  dih1  40985  dihmeetlem4preN  41005