Theorem releqd 5759

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916  df-rel 5662

This theorem is used by:  dftpos3  8243  tposfo2  8248  tposf12  8250  relexp0rel  15111  relexprelg  15112  relexpreld  15114  relexpaddg  15127  imasaddfnlem  17615  imasvscafn  17624  cicer  17896  joindmss  18466  meetdmss  18480  mattpostpos  22677  cnextrel  24290  perpln1  29065  perpln2  29066  erler  33706  opprabs  33885  relfae  34759  satfrel  35947  relecxrn  39156  dibvalrel  42037  dicvalrelN  42059  diclspsn  42068  dihvalrel  42153  dih1  42160  dihmeetlem4preN  42180  relcic  49972  oppfvalg  50053  oppfvallem  50062  funcoppc3  50074  uptposlem  50124  reldmprcof1  50308  reldmprcof2  50309  reldmlan2  50544  reldmran2  50545  rellan  50550  relran  50551