Theorem releq 5083

Description: Equality theorem for the relation predicate. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
releq	|- ( A = B -> ( Rel A <-> Rel B ) )

Proof of Theorem releq

Step	Hyp	Ref	Expression
1		sseq1 3525	. 2 |- ( A = B -> ( A C_ ( _V X. _V ) <-> B C_ ( _V X. _V ) ) )
2		df-rel 5006	. 2 |- ( Rel A <-> A C_ ( _V X. _V ) )
3		df-rel 5006	. 2 |- ( Rel B <-> B C_ ( _V X. _V ) )
4	1, 2, 3	3bitr4g 288	1 |- ( A = B -> ( Rel A <-> Rel B ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   _Vcvv 3113   C_ wss 3476   X. cxp 4997   Rel wrel 5004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-rel 5006

This theorem is referenced by:  releqi  5084  releqd  5085  dfrel2  5455  tposfn2  6974  ereq1  7315  isps  15685  isdir  15715  fpwrelmapffslem  27227  relexprel  28532  frrlem6  28973  prtlem12  30212  bnj1321  33162