Theorem releq 5644

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536  Vcvv 3491   ⊆ wss 3929   × cxp 5546  Rel wrel 5553

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2792

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2799  df-cleq 2813  df-clel 2892  df-in 3936  df-ss 3945  df-rel 5555

This theorem is referenced by:  releqi  5645  releqd  5646  relsnb  5668  dfrel2  6039  tposfn2  7907  ereq1  8289  isps  17807  isdir  17837  fpwrelmapffslem  30468  bnj1321  32320  refreleq  35793  symreleq  35827  trreleq  35851  prtlem12  36036  relintabex  40015  clrellem  40056  clcnvlem  40057