Theorem treq

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

	Ref	Expression
Assertion	treq	$$⊢A=B\to \left(\mathrm{Tr}A\leftrightarrow \mathrm{Tr}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		unieq	$$⊢A=B\to \bigcup A=\bigcup B$$
2	1	sseq1d	$$⊢A=B\to \left(\bigcup A\subseteq A\leftrightarrow \bigcup B\subseteq A\right)$$
3		sseq2	$$⊢A=B\to \left(\bigcup B\subseteq A\leftrightarrow \bigcup B\subseteq B\right)$$
4	2 3	bitrd	$$⊢A=B\to \left(\bigcup A\subseteq A\leftrightarrow \bigcup B\subseteq B\right)$$
5		df-tr	$$⊢\mathrm{Tr}A\leftrightarrow \bigcup A\subseteq A$$
6		df-tr	$$⊢\mathrm{Tr}B\leftrightarrow \bigcup B\subseteq B$$
7	4 5 6	3bitr4g	$$⊢A=B\to \left(\mathrm{Tr}A\leftrightarrow \mathrm{Tr}B\right)$$