Theorem releq 5753

Description: Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
releq	⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))

Proof of Theorem releq

Step	Hyp	Ref	Expression
1		sseq1 3934	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V)))
2		df-rel 5657	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
3		df-rel 5657	. 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
4	1, 2, 3	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1569  Vcvv 3450   ⊆ wss 3896   × cxp 5648  Rel wrel 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897  df-rel 5657

This theorem is used by:  releqi  5754  releqd  5755  relsnb  5780  dfrel2  6182  cnveq0b  6193  tposfn2  8270  ereq1  8730  isps  18749  isdir  18779  fpwrelmapffslem  33372  bnj1321  35705  refreleq  39640  symreleq  39681  trreleq  39705  prtlem12  40031  relintabex  44689  clrellem  44729  clcnvlem  44730  rellan  50913  relran  50914