Theorem releq 5765

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  Vcvv 3457   ⊆ wss 3906   × cxp 5661  Rel wrel 5668

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 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923  df-rel 5670

This theorem is used by:  releqi  5766  releqd  5767  relsnb  5791  dfrel2  6189  tposfn2  8246  ereq1  8704  isps  18642  isdir  18672  fpwrelmapffslem  33123  bnj1321  35456  refreleq  39283  symreleq  39324  trreleq  39348  prtlem12  39674  relintabex  44340  clrellem  44381  clcnvlem  44382  rellan  50434  relran  50435