Theorem releqd 5736

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  Rel wrel 5637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920  df-rel 5639

This theorem is referenced by:  dftpos3  8196  tposfo2  8201  tposf12  8203  relexp0rel  14972  relexprelg  14973  relexpreld  14975  relexpaddg  14988  imasaddfnlem  17461  imasvscafn  17470  cicer  17742  joindmss  18312  meetdmss  18326  mattpostpos  22410  cnextrel  24019  perpln1  28794  perpln2  28795  erler  33359  opprabs  33575  relfae  34425  satfrel  35583  relecxrn  38658  dibvalrel  41539  dicvalrelN  41561  diclspsn  41570  dihvalrel  41655  dih1  41662  dihmeetlem4preN  41682  relcic  49404  oppfvalg  49485  oppfvallem  49494  funcoppc3  49506  uptposlem  49556  reldmprcof1  49740  reldmprcof2  49741  reldmlan2  49976  reldmran2  49977  rellan  49982  relran  49983