Theorem dftr2

Description: An alternate way of defining a transitive class. Exercise 7 of TakeutiZaring p. 40. (Contributed by NM, 24-Apr-1994)

	Ref	Expression
Assertion	dftr2	|- ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )

Proof

Step	Hyp	Ref	Expression
1		dfss2	|- ( U. A C_ A <-> A. x ( x e. U. A -> x e. A ) )
2		df-tr	|- ( Tr A <-> U. A C_ A )
3		19.23v	|- ( A. y ( ( x e. y /\ y e. A ) -> x e. A ) <-> ( E. y ( x e. y /\ y e. A ) -> x e. A ) )
4		eluni	|- ( x e. U. A <-> E. y ( x e. y /\ y e. A ) )
5	4	imbi1i	|- ( ( x e. U. A -> x e. A ) <-> ( E. y ( x e. y /\ y e. A ) -> x e. A ) )
6	3 5	bitr4i	|- ( A. y ( ( x e. y /\ y e. A ) -> x e. A ) <-> ( x e. U. A -> x e. A ) )
7	6	albii	|- ( A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) <-> A. x ( x e. U. A -> x e. A ) )
8	1 2 7	3bitr4i	|- ( Tr A <-> A. x A. y ( ( x e. y /\ y e. A ) -> x e. A ) )