Theorem releq 5733

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  Vcvv 3429   ⊆ wss 3889   × cxp 5629  Rel wrel 5636

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906  df-rel 5638

This theorem is referenced by:  releqi  5734  releqd  5735  relsnb  5758  dfrel2  6153  tposfn2  8198  ereq1  8651  isps  18534  isdir  18564  fpwrelmapffslem  32805  bnj1321  35169  refreleq  38922  symreleq  38963  trreleq  38987  prtlem12  39313  relintabex  44008  clrellem  44049  clcnvlem  44050  rellan  50098  relran  50099