Theorem releqd 5763

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 5761	. 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 5663

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901  df-rel 5665

This theorem is used by:  dftpos3  8299  tposfo2  8304  tposf12  8306  relexp0rel  15233  relexprelg  15234  relexpreld  15236  relexpaddg  15249  imasaddfnlem  17750  imasvscafn  17759  cicer  18031  joindmss  18601  meetdmss  18615  mattpostpos  22824  cnextrel  24437  perpln1  29242  perpln2  29243  erler  33925  opprabs  34110  relfae  34991  satfrel  36340  relecxrn  39605  dibvalrel  42486  dicvalrelN  42508  diclspsn  42517  dihvalrel  42602  dih1  42609  dihmeetlem4preN  42629  relcic  50490  oppfvalg  50573  oppfvallem  50582  funcoppc3  50594  uptposlem  50644  reldmprcof1  50847  reldmprcof2  50848  reldmlan2  51131  reldmran2  51132  rellan  51137  relran  51138