Theorem uniinn0

Description: Sufficient and necessary condition for a union to intersect with a given set. (Contributed by Thierry Arnoux, 27-Jan-2020)

	Ref	Expression
Assertion	uniinn0	|- ( ( U. A i^i B ) =/= (/) <-> E. x e. A ( x i^i B ) =/= (/) )

Proof

Step	Hyp	Ref	Expression
1		nne	|- ( -. ( x i^i B ) =/= (/) <-> ( x i^i B ) = (/) )
2	1	ralbii	|- ( A. x e. A -. ( x i^i B ) =/= (/) <-> A. x e. A ( x i^i B ) = (/) )
3		ralnex	|- ( A. x e. A -. ( x i^i B ) =/= (/) <-> -. E. x e. A ( x i^i B ) =/= (/) )
4		unissb	|- ( U. A C_ ( _V \ B ) <-> A. x e. A x C_ ( _V \ B ) )
5		disj2	|- ( ( U. A i^i B ) = (/) <-> U. A C_ ( _V \ B ) )
6		disj2	|- ( ( x i^i B ) = (/) <-> x C_ ( _V \ B ) )
7	6	ralbii	|- ( A. x e. A ( x i^i B ) = (/) <-> A. x e. A x C_ ( _V \ B ) )
8	4 5 7	3bitr4ri	|- ( A. x e. A ( x i^i B ) = (/) <-> ( U. A i^i B ) = (/) )
9	2 3 8	3bitr3i	|- ( -. E. x e. A ( x i^i B ) =/= (/) <-> ( U. A i^i B ) = (/) )
10	9	necon1abii	|- ( ( U. A i^i B ) =/= (/) <-> E. x e. A ( x i^i B ) =/= (/) )