Theorem dftr3

Description: An alternate way of defining a transitive class. Definition 7.1 of TakeutiZaring p. 35. (Contributed by NM, 29-Aug-1993)

	Ref	Expression
Assertion	dftr3	$$⊢\mathrm{Tr}A\leftrightarrow \forall x\in Ax\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		dftr5	$$⊢\mathrm{Tr}A\leftrightarrow \forall x\in A\forall y\in xy\in A$$
2		dfss3	$$⊢x\subseteq A\leftrightarrow \forall y\in xy\in A$$
3	2	ralbii	$$⊢\forall x\in Ax\subseteq A\leftrightarrow \forall x\in A\forall y\in xy\in A$$
4	1 3	bitr4i	$$⊢\mathrm{Tr}A\leftrightarrow \forall x\in Ax\subseteq A$$