Theorem dftr2

Description: An alternate way of defining a transitive class. Exercise 7 of TakeutiZaring p. 40. Using dftr2c instead may avoid dependences on ax-11 . (Contributed by NM, 24-Apr-1994)

	Ref	Expression
Assertion	dftr2	$$⊢\mathrm{Tr}A\leftrightarrow \forall x\forall y\left(\left(x\in y\wedge y\in A\right)\to x\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$$⊢\bigcup A\subseteq A\leftrightarrow \forall x\left(x\in \bigcup A\to x\in A\right)$$
2		df-tr	$$⊢\mathrm{Tr}A\leftrightarrow \bigcup A\subseteq A$$
3		19.23v	$$⊢\forall y\left(\left(x\in y\wedge y\in A\right)\to x\in A\right)\leftrightarrow \left(\exists y\left(x\in y\wedge y\in A\right)\to x\in A\right)$$
4		eluni	$$⊢x\in \bigcup A\leftrightarrow \exists y\left(x\in y\wedge y\in A\right)$$
5	4	imbi1i	$$⊢\left(x\in \bigcup A\to x\in A\right)\leftrightarrow \left(\exists y\left(x\in y\wedge y\in A\right)\to x\in A\right)$$
6	3 5	bitr4i	$$⊢\forall y\left(\left(x\in y\wedge y\in A\right)\to x\in A\right)\leftrightarrow \left(x\in \bigcup A\to x\in A\right)$$
7	6	albii	$$⊢\forall x\forall y\left(\left(x\in y\wedge y\in A\right)\to x\in A\right)\leftrightarrow \forall x\left(x\in \bigcup A\to x\in A\right)$$
8	1 2 7	3bitr4i	$$⊢\mathrm{Tr}A\leftrightarrow \forall x\forall y\left(\left(x\in y\wedge y\in A\right)\to x\in A\right)$$