Theorem treq

Description: Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993)

	Ref	Expression
Assertion	treq	|- ( A = B -> ( Tr A <-> Tr B ) )

Proof

Step	Hyp	Ref	Expression
1		unieq	|- ( A = B -> U. A = U. B )
2	1	sseq1d	|- ( A = B -> ( U. A C_ A <-> U. B C_ A ) )
3		sseq2	|- ( A = B -> ( U. B C_ A <-> U. B C_ B ) )
4	2 3	bitrd	|- ( A = B -> ( U. A C_ A <-> U. B C_ B ) )
5		df-tr	|- ( Tr A <-> U. A C_ A )
6		df-tr	|- ( Tr B <-> U. B C_ B )
7	4 5 6	3bitr4g	|- ( A = B -> ( Tr A <-> Tr B ) )