Theorem releq 5726

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  Vcvv 3430   ⊆ wss 3890   × cxp 5622  Rel wrel 5629

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 3907  df-rel 5631

This theorem is referenced by:  releqi  5727  releqd  5728  relsnb  5751  dfrel2  6147  tposfn2  8191  ereq1  8644  isps  18525  isdir  18555  fpwrelmapffslem  32820  bnj1321  35185  refreleq  38936  symreleq  38977  trreleq  39001  prtlem12  39327  relintabex  44026  clrellem  44067  clcnvlem  44068  rellan  50110  relran  50111