Theorem eltrans

Description: Membership in the class of all transitive sets. (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Hypothesis	eltrans.1	|- A e. _V
Assertion	eltrans	|- ( A e. Trans <-> Tr A )

Proof

Step	Hyp	Ref	Expression
1		eltrans.1	|- A e. _V
2		df-trans	|- Trans = ( _V \ ran ( ( _E o. _E ) \ _E ) )
3	2	eleq2i	|- ( A e. Trans <-> A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) )
4	1	dftr6	|- ( Tr A <-> A e. ( _V \ ran ( ( _E o. _E ) \ _E ) ) )
5	3 4	bitr4i	|- ( A e. Trans <-> Tr A )