Theorem releqd 5741

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

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

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 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931  df-rel 5645

This theorem is referenced by:  dftpos3  8223  tposfo2  8228  tposf12  8230  relexp0rel  15003  relexprelg  15004  relexpreld  15006  relexpaddg  15019  imasaddfnlem  17491  imasvscafn  17500  cicer  17768  joindmss  18338  meetdmss  18352  mattpostpos  22341  cnextrel  23950  perpln1  28637  perpln2  28638  erler  33216  opprabs  33453  relfae  34237  satfrel  35354  dibvalrel  41157  dicvalrelN  41179  diclspsn  41188  dihvalrel  41273  dih1  41280  dihmeetlem4preN  41300  relcic  49034  oppfvalg  49115  oppfvallem  49124  funcoppc3  49136  uptposlem  49186  reldmprcof1  49370  reldmprcof2  49371  reldmlan2  49606  reldmran2  49607  rellan  49612  relran  49613