Theorem releq 5724

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  Vcvv 3438   ⊆ wss 3905   × cxp 5621  Rel wrel 5628

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 3922  df-rel 5630

This theorem is referenced by:  releqi  5725  releqd  5726  relsnb  5749  dfrel2  6142  tposfn2  8188  ereq1  8639  isps  18492  isdir  18522  fpwrelmapffslem  32688  bnj1321  34996  refreleq  38500  symreleq  38537  trreleq  38561  prtlem12  38848  relintabex  43557  clrellem  43598  clcnvlem  43599  rellan  49612  relran  49613