Theorem untuni

Description: The union of a class is untangled iff all its members are untangled. (Contributed by Scott Fenton, 28-Feb-2011)

	Ref	Expression
Assertion	untuni	|- ( A. x e. U. A -. x e. x <-> A. y e. A A. x e. y -. x e. x )

Proof

Step	Hyp	Ref	Expression
1		r19.23v	|- ( A. y e. A ( x e. y -> -. x e. x ) <-> ( E. y e. A x e. y -> -. x e. x ) )
2	1	albii	|- ( A. x A. y e. A ( x e. y -> -. x e. x ) <-> A. x ( E. y e. A x e. y -> -. x e. x ) )
3		ralcom4	|- ( A. y e. A A. x ( x e. y -> -. x e. x ) <-> A. x A. y e. A ( x e. y -> -. x e. x ) )
4		eluni2	|- ( x e. U. A <-> E. y e. A x e. y )
5	4	imbi1i	|- ( ( x e. U. A -> -. x e. x ) <-> ( E. y e. A x e. y -> -. x e. x ) )
6	5	albii	|- ( A. x ( x e. U. A -> -. x e. x ) <-> A. x ( E. y e. A x e. y -> -. x e. x ) )
7	2 3 6	3bitr4ri	|- ( A. x ( x e. U. A -> -. x e. x ) <-> A. y e. A A. x ( x e. y -> -. x e. x ) )
8		df-ral	|- ( A. x e. U. A -. x e. x <-> A. x ( x e. U. A -> -. x e. x ) )
9		df-ral	|- ( A. x e. y -. x e. x <-> A. x ( x e. y -> -. x e. x ) )
10	9	ralbii	|- ( A. y e. A A. x e. y -. x e. x <-> A. y e. A A. x ( x e. y -> -. x e. x ) )
11	7 8 10	3bitr4i	|- ( A. x e. U. A -. x e. x <-> A. y e. A A. x e. y -. x e. x )