Theorem releqd 5755

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 5753	. 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 5656

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 2733

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

This theorem is used by:  dftpos3  8261  tposfo2  8266  tposf12  8268  relexp0rel  15190  relexprelg  15191  relexpreld  15193  relexpaddg  15206  imasaddfnlem  17700  imasvscafn  17709  cicer  17981  joindmss  18551  meetdmss  18565  mattpostpos  22769  cnextrel  24382  perpln1  29185  perpln2  29186  erler  33826  opprabs  34006  relfae  34880  satfrel  36132  relecxrn  39339  dibvalrel  42220  dicvalrelN  42242  diclspsn  42251  dihvalrel  42336  dih1  42343  dihmeetlem4preN  42363  relcic  50152  oppfvalg  50233  oppfvallem  50242  funcoppc3  50254  uptposlem  50304  reldmprcof1  50488  reldmprcof2  50489  reldmlan2  50724  reldmran2  50725  rellan  50730  relran  50731