Theorem releq 5745

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 3959	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ (V × V) ↔ 𝐵 ⊆ (V × V)))
2		df-rel 5650	. 2 ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))
3		df-rel 5650	. 2 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
4	1, 2, 3	3bitr4g 316	1 ⊢ (𝐴 = 𝐵 → (Rel 𝐴 ↔ Rel 𝐵))

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  Vcvv 3453   ⊆ wss 3902   × cxp 5641  Rel wrel 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919  df-rel 5650

This theorem is referenced by:  releqi  5746  releqd  5747  relsnb  5771  dfrel2  6170  tposfn2  8222  ereq1  8680  isps  18591  isdir  18621  fpwrelmapffslem  32895  bnj1321  35283  refreleq  39061  symreleq  39102  trreleq  39126  prtlem12  39452  relintabex  44118  clrellem  44159  clcnvlem  44160  rellan  50205  relran  50206