Theorem untangtr

Description: A transitive class is untangled iff its elements are. (Contributed by Scott Fenton, 7-Mar-2011)

	Ref	Expression
Assertion	untangtr	|- ( Tr A -> ( A. x e. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) )

Proof

Step	Hyp	Ref	Expression
1		df-tr	|- ( Tr A <-> U. A C_ A )
2		ssralv	|- ( U. A C_ A -> ( A. x e. A -. x e. x -> A. x e. U. A -. x e. x ) )
3	1 2	sylbi	|- ( Tr A -> ( A. x e. A -. x e. x -> A. x e. U. A -. x e. x ) )
4		elequ1	|- ( x = y -> ( x e. x <-> y e. x ) )
5		elequ2	|- ( x = y -> ( y e. x <-> y e. y ) )
6	4 5	bitrd	|- ( x = y -> ( x e. x <-> y e. y ) )
7	6	notbid	|- ( x = y -> ( -. x e. x <-> -. y e. y ) )
8	7	cbvralvw	|- ( A. x e. U. A -. x e. x <-> A. y e. U. A -. y e. y )
9		untuni	|- ( A. y e. U. A -. y e. y <-> A. x e. A A. y e. x -. y e. y )
10	8 9	bitri	|- ( A. x e. U. A -. x e. x <-> A. x e. A A. y e. x -. y e. y )
11	3 10	imbitrdi	|- ( Tr A -> ( A. x e. A -. x e. x -> A. x e. A A. y e. x -. y e. y ) )
12		untelirr	|- ( A. y e. x -. y e. y -> -. x e. x )
13	12	ralimi	|- ( A. x e. A A. y e. x -. y e. y -> A. x e. A -. x e. x )
14	11 13	impbid1	|- ( Tr A -> ( A. x e. A -. x e. x <-> A. x e. A A. y e. x -. y e. y ) )